update satsolve dimacs test dofile and comment out minisat/Global.h o…

…perator overload !=
DVLab-NTU · Oct 6, 2024 · 06717c2 · 06717c2
1 parent 71cae5e
commit 06717c2
Show file tree

Hide file tree

Showing 8 changed files with 382 additions and 1 deletion.
diff --git a/satsolvers/minisat/Global.h b/satsolvers/minisat/Global.h
@@ -275,7 +275,7 @@ const gvlbool gv_l_Undef = toLbool( 0);
 
 #ifndef __SGI_STL_INTERNAL_RELOPS   // (be aware of SGI's STL implementation...)
 #define __SGI_STL_INTERNAL_RELOPS
-template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
+// template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
 template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
 template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
 template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }

diff --git a/testbench/dimacs_sat.txt b/testbench/dimacs_sat.txt
@@ -0,0 +1,151 @@
+p cnf 60 150
+16 -53 32 -9 0
+-17 -52 0
+-53 32 -45 2 0
+43 8 -20 0
+51 -17 26 -57 0
+17 -43 0
+54 30 -4 10 0
+-42 5 20 -17 0
+34 -30 -36 0
+-60 30 -13 0
+18 -17 -58 -1 0
+14 -29 -36 0
+-57 19 6 0
+47 33 0
+-28 -11 51 0
+-60 -59 0
+-2 -1 -45 37 0
+-50 4 -10 0
+30 26 0
+-8 -17 19 0
+44 -8 0
+14 -2 8 0
+5 45 -51 0
+-16 -39 -49 0
+56 -2 0
+-47 47 0
+-38 -60 34 32 0
+-30 5 0
+-25 17 -11 -49 0
+47 -23 11 -59 0
+-58 20 23 0
+51 31 40 -3 0
+-25 13 0
+46 -16 -26 0
+40 -32 -7 0
+19 -41 -35 0
+-35 24 30 -33 0
+-47 40 0
+38 -43 -41 -17 0
+-50 -18 60 0
+-43 57 39 0
+-53 -21 -52 -58 0
+-49 -31 0
+-38 -41 0
+-38 -31 0
+-1 37 12 34 0
+-14 -59 -9 45 0
+-23 -42 -25 -43 0
+55 44 -52 -20 0
+-2 -59 0
+-22 44 26 47 0
+21 5 0
+29 45 -39 -38 0
+-43 -25 -32 0
+-19 23 10 0
+-33 20 15 0
+18 32 23 0
+-33 -26 0
+13 -20 -53 6 0
+51 -48 0
+-56 41 -34 0
+-48 58 55 0
+25 50 0
+46 -6 43 58 0
+57 -30 -13 0
+-43 -14 -40 0
+-27 -60 -9 31 0
+2 44 50 0
+-48 6 0
+-8 33 42 0
+-57 -18 -40 6 0
+-8 -26 -6 -54 0
+46 -32 0
+32 -11 0
+27 53 -32 -32 0
+58 -55 51 0
+-31 30 -21 0
+-37 9 -30 0
+42 -6 -59 23 0
+16 -49 24 20 0
+3 -15 -15 -4 0
+-22 58 0
+-35 -39 -29 26 0
+28 11 0
+39 24 -60 0
+-14 -54 -53 -54 0
+55 27 0
+49 -35 0
+12 -48 -10 0
+-21 4 52 -50 0
+14 54 2 -42 0
+42 -5 26 0
+-18 24 30 0
+-3 1 0
+33 30 -51 0
+40 -9 -45 -32 0
+-34 23 0
+27 59 -4 0
+-39 6 0
+42 23 -32 0
+29 -55 -15 -59 0
+13 -30 0
+45 58 -33 4 0
+-34 34 0
+-53 -23 -23 54 0
+-14 11 17 0
+7 -5 0
+51 -12 32 0
+3 16 0
+-24 -15 0
+-7 39 0
+41 39 -22 0
+-40 -31 0
+-40 12 -7 -24 0
+-3 3 0
+60 -51 0
+-52 -23 47 0
+38 -36 5 0
+50 21 0
+39 43 -34 0
+-6 -20 -42 -14 0
+-55 -8 32 0
+-41 21 -18 0
+38 12 0
+-38 52 3 -27 0
+20 29 24 36 0
+-42 -39 5 -42 0
+21 -36 30 -25 0
+-23 -42 0
+4 -37 0
+21 -59 -15 55 0
+-39 -13 -41 13 0
+7 -38 37 52 0
+-2 23 20 5 0
+-37 -25 0
+38 46 15 0
+-59 55 0
+-29 -25 -40 -37 0
+-15 -7 37 -46 0
+51 44 -33 0
+46 17 0
+3 54 6 19 0
+-56 17 -9 -57 0
+-47 31 38 -17 0
+60 -59 -59 0
+-56 -21 0
+35 -26 52 -2 0
+-24 -52 8 0
+29 -14 4 -57 0
+41 -41 0
diff --git a/testbench/dimacs_unsat.txt b/testbench/dimacs_unsat.txt
@@ -0,0 +1,202 @@
+p cnf 60 200
+-22 -26 -55 0
+-42 -39 48 -4 0
+-59 -33 -49 -54 0
+-30 7 -51 -55 0
+20 23 0
+58 -59 0
+16 -4 -47 -16 0
+38 36 26 0
+37 45 17 -3 0
+12 -19 -15 0
+-31 23 0
+-8 60 0
+-30 -26 -2 0
+38 -33 0
+-40 52 0
+58 11 60 -24 0
+30 17 0
+38 -38 0
+11 18 -42 20 0
+8 -49 0
+55 53 -42 7 0
+-13 41 0
+49 38 51 2 0
+-38 -24 -35 0
+-22 -29 0
+32 11 -41 25 0
+52 -38 0
+-33 58 -7 0
+57 32 -17 28 0
+51 27 -26 31 0
+32 -2 -3 0
+10 -34 0
+15 57 40 15 0
+-50 56 -10 -22 0
+-30 30 15 3 0
+45 15 0
+53 55 -28 35 0
+-47 17 47 0
+60 -40 0
+36 -54 43 4 0
+23 -49 -58 14 0
+-26 59 -1 -35 0
+-39 -36 0
+32 -51 40 51 0
+42 -15 6 4 0
+31 22 3 0
+-28 -32 0
+-47 30 5 6 0
+16 52 48 -10 0
+5 21 -42 -37 0
+35 -45 34 50 0
+-50 -47 0
+30 22 0
+-28 18 14 0
+-44 50 0
+24 -12 -5 0
+-31 -39 -4 0
+33 19 -47 -40 0
+56 30 0
+22 -56 0
+-48 53 0
+-44 -32 -10 0
+-44 29 0
+24 38 0
+-12 54 -37 0
+55 38 38 0
+8 14 -59 0
+-35 12 0
+48 48 0
+-36 -33 -13 -1 0
+45 -59 0
+-25 20 29 0
+27 -1 7 49 0
+-55 -40 -29 0
+-25 -17 20 -6 0
+18 32 22 0
+-49 18 -38 -16 0
+-22 -50 0
+-30 10 0
+50 25 0
+21 -7 16 51 0
+-11 -33 -26 0
+-11 -3 -52 0
+-37 -34 15 0
+41 -57 31 8 0
+-36 1 -2 -56 0
+-27 27 0
+-47 -1 -6 55 0
+43 -50 44 -34 0
+34 18 46 0
+27 -38 -56 1 0
+55 20 0
+42 -2 0
+56 33 4 -7 0
+-47 -11 0
+53 46 0
+19 32 -41 0
+34 35 -9 0
+-46 -44 31 0
+-10 -50 0
+-16 -30 32 0
+37 -15 56 -30 0
+28 29 -50 24 0
+-33 -28 0
+28 44 -23 32 0
+7 34 -31 0
+51 -3 -29 0
+-24 37 25 -38 0
+5 -46 -37 0
+-44 2 -26 0
+26 8 29 21 0
+-17 -48 32 0
+35 59 51 0
+17 25 6 -29 0
+-11 -2 27 0
+-4 -46 0
+12 -59 0
+60 37 -3 54 0
+-40 18 0
+-29 22 -8 0
+53 -57 -46 0
+-59 8 0
+-32 -16 -46 0
+-54 -31 40 0
+-24 -3 18 -20 0
+31 -57 -15 -17 0
+-22 16 49 0
+22 20 26 -44 0
+-15 -23 9 0
+26 -22 0
+-32 11 -31 0
+17 3 10 0
+-43 -44 38 19 0
+-12 40 5 0
+-22 -43 0
+50 -27 3 0
+35 6 0
+-14 53 -25 0
+-10 -28 19 0
+18 7 5 0
+30 29 -4 45 0
+-16 -43 0
+-43 16 0
+-41 9 39 0
+49 26 55 0
+-29 44 -24 0
+-60 9 0
+40 -16 1 26 0
+57 -12 0
+39 -45 46 0
+-29 59 -35 0
+39 1 -48 -42 0
+-26 44 55 0
+-11 56 0
+26 -26 -11 -42 0
+52 23 -32 -43 0
+-25 -28 0
+-57 41 0
+-51 -7 -46 0
+-39 -6 0
+-3 -37 -33 40 0
+28 41 -15 0
+15 -40 18 2 0
+30 -24 2 0
+-29 36 -50 -34 0
+-10 -42 -12 58 0
+-41 -2 51 0
+-25 57 -29 0
+45 -45 0
+39 -45 17 0
+-46 44 -37 -12 0
+-19 -59 0
+15 -46 47 -14 0
+50 58 16 2 0
+-24 28 0
+5 41 0
+49 -54 -25 -13 0
+-48 13 47 -15 0
+-22 -54 -48 0
+31 -12 0
+-30 -54 0
+48 -5 0
+58 -37 5 0
+25 -36 -56 0
+-55 55 60 0
+-50 18 -4 -3 0
+-21 -58 4 0
+30 -40 37 -36 0
+-7 -42 49 0
+-55 -53 -53 0
+60 -5 0
+-41 -3 -59 0
+2 5 0
+-1 37 0
+54 30 0
+11 -51 0
+16 6 0
+24 -23 28 53 0
+-29 -18 -18 -17 0
+-47 -13 4 60 0
+
diff --git a/tests/common/ref_linux/help.log b/tests/common/ref_linux/help.log
@@ -45,6 +45,9 @@ BSIMulate:          BDD simulation
 BXNOR:              BDD Xnor
 BXOR:               BDD Xor
 
+========== SATSolving Commands : ==========
+SATSolve DIMACS:    Command for satsolving DIMACS format file.
+
 ========== EXP Commands : ==========
 EXPeriment:         Command for the testing of the experimental functions.
 

diff --git a/tests/sat/dofile/satsolve_dimacs_sat.dofile b/tests/sat/dofile/satsolve_dimacs_sat.dofile
@@ -0,0 +1,2 @@
+satsolve dimacs -file ./testbench/dimacs_sat.txt
+q -f
diff --git a/tests/sat/dofile/satsolve_dimacs_unsat.dofile b/tests/sat/dofile/satsolve_dimacs_unsat.dofile
@@ -0,0 +1,2 @@
+satsolve dimacs -file ./testbench/dimacs_unsat.txt
+q -f
diff --git a/tests/sat/ref_linux/satsolve_dimacs_sat.log b/tests/sat/ref_linux/satsolve_dimacs_sat.log
@@ -0,0 +1,11 @@
+setup> satsolve dimacs -file ./testbench/dimacs_sat.txt
+==================================[MINISAT]===================================
+| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
+|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
+==============================================================================
+|         0 |     145      439 |      48       0        0    -nan |  0.000 % |
+==============================================================================
+SAT
+-1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 12 13 -14 -15 16 -17 -18 -19 -20 21 -22 23 24 25 26 27 -28 -29 -30 -31 32 -33 -34 -35 -36 -37 -38 -39 40 -41 -42 -43 44 -45 46 47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 
+setup> q -f
+
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		satsolve dimacs -file ./testbench/dimacs_sat.txt
		q -f