Modified the examples to work w/ the new markbdd format features.

fett · fett · commit 5af6c406b3e0 · 2007-06-19T02:28:30.000Z
Worked on the user manual a tad.

   ~Sean
diff --git a/doc/manual/sbsat_user_manual.tex b/doc/manual/sbsat_user_manual.tex
@@ -900,11 +900,11 @@ \subsection{An input in canonical (BDD) form}\label{can-section}
 \vspace*{-3mm}\\
 \indent{\tt imp(-x3, -x4)}\\
 \indent{\tt xor(x1, -x5)}\\
-\indent{\tt xor6(x8, x3, -x2, x7, -x4, -x1)}
+\indent{\tt xor(x8, x3, -x2, x7, -x4, -x1)}
 
 \noindent
 \textbf{\underbar{Remark}}: ~Since no extension of a binary function 
-can take 1 argument, {\tt xor1(-x1)} is not admitted.
+can take 1 argument, {\tt xor(-x1)} is not admitted.
 
 A function argument may be a variable, a function, or a reference to a
 function defined elsewhere in the file.  To support the latter, every
@@ -924,14 +924,14 @@ \subsection{An input in canonical (BDD) form}\label{can-section}
 {\tt or(x2, x3)}\\
 {\tt and(x3, x4)}\\
 {\tt imp(x3, \$2)}\\
-{\tt xor4(\$3, \$1, x4, x1)}\\
+{\tt xor(\$3, \$1, x4, x1)}\\
 {\tt and(x2, x3)}\\
 }
 
 \noindent
 The fourth line of this group is equivalent to\\
 \vspace*{-3mm}\\
-\indent{\tt xor4(imp(x3, and(x3, x4)), or(x2, x3), x4, x1)}\\
+\indent{\tt xor(imp(x3, and(x3, x4)), or(x2, x3), x4, x1)}\\
 \vspace*{-3mm}\\
 which is {\em also} recognized by {\tt sbsat}.
 
@@ -946,8 +946,7 @@ \subsection{An input in canonical (BDD) form}\label{can-section}
 {\tt or(x2, x3)}\\
 {\tt and(x3, x4)}\\
 {\tt imp(x3, \$2)}\\
-{\tt ; The next line is the first *ed line of the file}\\
-{\tt *xor4(\$3, \$1, x4, x1)}\\
+{\tt *xor(\$3, \$1, x4, x1)}\\
 {\tt *or(x2, x3)}\\
 }
 
diff --git a/examples/add_state.ite b/examples/add_state.ite
@@ -1,8 +1,8 @@
 p bdd 19 5
 #define add_state(var1, var2, var3, var4, var5)
 #equ(xor(var1, and(-var2, var3)), ite(var4, or(var5, -var3), -var3))
-*add_state(1, 3, 5, 9 ,10)
-*add_state(2, 4, 6, 10 ,11)
-*add_state(3, 5, 7, 11 ,12)
-*add_state(4, 6, 8, 12 ,13)
-*add_state(5, 7, 9, 13 ,14)
+add_state(1, 3, 5, 9 ,10)
+add_state(2, 4, 6, 10 ,11)
+add_state(3, 5, 7, 11 ,12)
+add_state(4, 6, 8, 12 ,13)
+add_state(5, 7, 9, 13 ,14)
diff --git a/examples/flowers.ite b/examples/flowers.ite
@@ -6,7 +6,7 @@ p bdd 4 4
 ;The question must be negated and added to the database.
 ;If SBSAT returns 'unsat' then the answer to the question
 ;is 'YES', otherwise the answer is 'NO'.
-imp(Coloured, Scented) ;
-imp(-OpenAir, -Like) ;
-imp(OpenAir, Coloured) ;
-not(imp(-Scented, -Like)) ;
+imp(Coloured, Scented)
+imp(-OpenAir, -Like)
+imp(OpenAir, Coloured)
+not(imp(-Scented, -Like))
diff --git a/examples/interconnect_example.ite b/examples/interconnect_example.ite
@@ -8,7 +8,7 @@ equ(o15, ite(s1, x11, x12))
 equ(o16, ite(s2, x14, x13))
 equ(x11, o11)
 ; Constraint forcing impulse(1)
-and4(-x11, x12, x13, x14)
+and(-x11, x12, x13, x14)
  
 ; Consistency constraints for impulse(3)
 equ(o21, ite(s1, x22, x21))
@@ -19,7 +19,7 @@ equ(o25, ite(s1, x21, x22))
 equ(o26, ite(s2, x24, x23))
 equ(x21, o21)
 ; Constraint forcing impulse(2)
-and4(x21, -x22, x23, x24)
+and(x21, -x22, x23, x24)
 
 ; Consistency constraints for impulse(3)
 equ(o31, ite(s1, x32, x31))
@@ -30,7 +30,7 @@ equ(o35, ite(s1, x31, x32))
 equ(o36, ite(s2, x34, x33))
 equ(x31, o31)
 ; Constraint forcing impulse(3)
-and4(x31, x32, -x33, x34)
+and(x31, x32, -x33, x34)
 
 ; Consistency constraints for impulse(4)
 equ(o41, ite(s1, x42, x41))
@@ -41,5 +41,5 @@ equ(o45, ite(s1, x41, x42))
 equ(o46, ite(s2, x44, x43))
 equ(x41, o41)
 ; Constraint forcing impulse(4)
-and4(x41, x42, x43, -x44)
+and(x41, x42, x43, -x44)
 
diff --git a/examples/minmax.ite b/examples/minmax.ite
@@ -1,11 +1,11 @@
 p bdd 20 9
 ; minmax.cnf is the cnf counterpart to this file.
-*minmax(4, 1, 3, 1, 6, 11, 16)
-*minmax(4, 1, 2, 2, 7, 12, 17)
-*minmax(4, 1, 1, 3, 8, 13, 18)
-*minmax(4, 2, 4, 4, 9, 14, 19)
-*minmax(4, 0, 1, 5, 10, 15, 20)
-*or5(-1, -2, -3, -4, -5)
-*or5(-6, -7, -8, -9, -10)
-*or5(-11, -12, -13, -14, -15)
-*or5(-16, -17, -18, -19, -20)
+minmax(1, 3, 1, 6, 11, 16)
+minmax(1, 2, 2, 7, 12, 17)
+minmax(1, 1, 3, 8, 13, 18)
+minmax(2, 4, 4, 9, 14, 19)
+minmax(0, 1, 5, 10, 15, 20)
+or(-1, -2, -3, -4, -5)
+or(-6, -7, -8, -9, -10)
+or(-11, -12, -13, -14, -15)
+or(-16, -17, -18, -19, -20)
diff --git a/examples/xortest.ite b/examples/xortest.ite
@@ -1,4 +1,4 @@
 p bdd 12 3
-*equ(xor3(123, 125, 156), F)
-*equ(xor(134, and3(155, 127, 167)), T)
-*equ(xor(and3(1, 2, 3), and3(45, 145, 167)), F)
+equ(xor(123, 125, 156), F)
+equ(xor(134, and(155, 127, 167)), T)
+equ(xor(and(1, 2, 3), and(45, 145, 167)), F)
diff --git a/src/formats/markbdd.cc b/src/formats/markbdd.cc
@@ -1230,7 +1230,7 @@ void bddloop () {
 			if(p==';') continue_all = 1;
 			else if (p!=' ' && p!='(' && p!=')' && p!=',') {
 				fprintf(stderr, "Error: Extra characters following line %d...exiting\n", markbdd_line);
-				exit(0);
+				exit (1);
 				continue_all = 1;
 			}
          p = fgetc(finputfile);
@@ -1240,7 +1240,7 @@ void bddloop () {
 				if (p == ';') continue_all = 1;
 				if (continue_all == 0 && p!=' ' && p!='(' && p!=')' && p!=',') {
 					fprintf(stderr, "Error: Extra characters following line %d...exiting\n", markbdd_line);
-					exit(0);
+					exit (1);
 					continue_all = 1;
 				}
             p = fgetc(finputfile);
diff --git a/tests/longer_tests/slider_80_sat.ite b/tests/longer_tests/slider_80_sat.ite
@@ -1,87 +1,87 @@
 p bdd 80 83
 #define add_state1(1, 15, 17, 33, 24, 40)
-#equ(xor3(1, and(-17, 33), nand(40, 24), ite(15, or(33, -40), -33))))
-*add_state1(1, 17, 15, 24, 33, 40) 
-*add_state1(2, 18, 16, 25, 34, 41) 
-*add_state1(3, 19, 17, 26, 35, 42) 
-*add_state1(4, 20, 18, 27, 36, 43) 
-*add_state1(5, 21, 19, 28, 37, 44) 
-*add_state1(6, 22, 20, 29, 38, 45) 
-*add_state1(7, 23, 21, 30, 39, 46) 
-*add_state1(8, 24, 22, 31, 40, 47) 
-*add_state1(9, 25, 23, 32, 41, 48) 
-*add_state1(10, 26, 24, 33, 42, 49) 
-*add_state1(11, 27, 25, 34, 43, 50) 
-*add_state1(12, 28, 26, 35, 44, 51) 
-*add_state1(13, 29, 27, 36, 45, 52) 
-*add_state1(14, 30, 28, 37, 46, 53) 
-*add_state1(15, 31, 29, 38, 47, 54) 
-*add_state1(16, 32, 30, 39, 48, 55) 
-*add_state1(17, 33, 31, 40, 49, 56) 
-*add_state1(18, 34, 32, 41, 50, 57) 
-*add_state1(19, 35, 33, 42, 51, 58) 
-*add_state1(20, 36, 34, 43, 52, 59) 
-*add_state1(21, 37, 35, 44, 53, 60) 
-*add_state1(22, 38, 36, 45, 54, 61) 
-*add_state1(23, 39, 37, 46, 55, 62) 
-*add_state1(24, 40, 38, 47, 56, 63) 
-*add_state1(25, 41, 39, 48, 57, 64) 
-*add_state1(26, 42, 40, 49, 58, 65) 
-*add_state1(27, 43, 41, 50, 59, 66) 
-*add_state1(28, 44, 42, 51, 60, 67) 
-*add_state1(29, 45, 43, 52, 61, 68) 
-*add_state1(30, 46, 44, 53, 62, 69) 
-*add_state1(31, 47, 45, 54, 63, 70) 
-*add_state1(32, 48, 46, 55, 64, 71) 
-*add_state1(33, 49, 47, 56, 65, 72) 
-*add_state1(34, 50, 48, 57, 66, 73) 
-*add_state1(35, 51, 49, 58, 67, 74) 
-*add_state1(36, 52, 50, 59, 68, 75) 
-*add_state1(37, 53, 51, 60, 69, 76) 
-*add_state1(38, 54, 52, 61, 70, 77)
-*add_state1(39, 55, 53, 62, 71, 78) 
-*add_state1(40, 56, 54, 63, 72, 79)
+#equ(xor(1, and(-17, 33), nand(40, 24)), ite(15, or(33, -40), -33))
+add_state1(1, 17, 15, 24, 33, 40) 
+add_state1(2, 18, 16, 25, 34, 41) 
+add_state1(3, 19, 17, 26, 35, 42) 
+add_state1(4, 20, 18, 27, 36, 43) 
+add_state1(5, 21, 19, 28, 37, 44) 
+add_state1(6, 22, 20, 29, 38, 45) 
+add_state1(7, 23, 21, 30, 39, 46) 
+add_state1(8, 24, 22, 31, 40, 47) 
+add_state1(9, 25, 23, 32, 41, 48) 
+add_state1(10, 26, 24, 33, 42, 49) 
+add_state1(11, 27, 25, 34, 43, 50) 
+add_state1(12, 28, 26, 35, 44, 51) 
+add_state1(13, 29, 27, 36, 45, 52) 
+add_state1(14, 30, 28, 37, 46, 53) 
+add_state1(15, 31, 29, 38, 47, 54) 
+add_state1(16, 32, 30, 39, 48, 55) 
+add_state1(17, 33, 31, 40, 49, 56) 
+add_state1(18, 34, 32, 41, 50, 57) 
+add_state1(19, 35, 33, 42, 51, 58) 
+add_state1(20, 36, 34, 43, 52, 59) 
+add_state1(21, 37, 35, 44, 53, 60) 
+add_state1(22, 38, 36, 45, 54, 61) 
+add_state1(23, 39, 37, 46, 55, 62) 
+add_state1(24, 40, 38, 47, 56, 63) 
+add_state1(25, 41, 39, 48, 57, 64) 
+add_state1(26, 42, 40, 49, 58, 65) 
+add_state1(27, 43, 41, 50, 59, 66) 
+add_state1(28, 44, 42, 51, 60, 67) 
+add_state1(29, 45, 43, 52, 61, 68) 
+add_state1(30, 46, 44, 53, 62, 69) 
+add_state1(31, 47, 45, 54, 63, 70) 
+add_state1(32, 48, 46, 55, 64, 71) 
+add_state1(33, 49, 47, 56, 65, 72) 
+add_state1(34, 50, 48, 57, 66, 73) 
+add_state1(35, 51, 49, 58, 67, 74) 
+add_state1(36, 52, 50, 59, 68, 75) 
+add_state1(37, 53, 51, 60, 69, 76) 
+add_state1(38, 54, 52, 61, 70, 77)
+add_state1(39, 55, 53, 62, 71, 78) 
+add_state1(40, 56, 54, 63, 72, 79)
 #define add_state2(1, 12, 16, 18, 27, 40)
-#xor3(-1, xor3(16, and(-18, 27), 18), equ(40, 12))
+#xor(-1, xor(16, and(-18, 27), 18), equ(40, 12))
 #define add_state3(1, 12, 16, 18, 27, 40)
-#xor3(-1, xor3(16, and(-18, 27), 18), equ(40, 12))
-*add_state2(1, 12, 16, 18, 27, 40)
-*add_state3(2, 13, 17, 19, 28, 41) 
-*add_state2(3, 14, 18, 20, 29, 42) 
-*add_state3(4, 15, 19, 21, 30, 43) 
-*add_state2(5, 16, 20, 22, 31, 44) 
-*add_state3(6, 17, 21, 23, 32, 45) 
-*add_state2(7, 18, 22, 24, 33, 46) 
-*add_state3(8, 19, 23, 25, 34, 47) 
-*add_state2(9, 20, 24, 26, 35, 48) 
-*add_state3(10, 21, 25, 27, 36, 49) 
-*add_state2(11, 22, 26, 28, 37, 50) 
-*add_state3(12, 23, 27, 29, 38, 51) 
-*add_state2(13, 24, 28, 30, 39, 52) 
-*add_state3(14, 25, 29, 31, 40, 53) 
-*add_state2(15, 26, 30, 32, 41, 54) 
-*add_state3(16, 27, 31, 33, 42, 55) 
-*add_state2(17, 28, 32, 34, 43, 56) 
-*add_state3(18, 29, 33, 35, 44, 57) 
-*add_state2(19, 30, 34, 36, 45, 58) 
-*add_state3(20, 31, 35, 37, 46, 59) 
-*add_state2(21, 32, 36, 38, 47, 60) 
-*add_state3(22, 33, 37, 39, 48, 61)
-*add_state2(23, 34, 38, 40, 49, 62) 
-*add_state3(24, 35, 39, 41, 50, 63) 
-*add_state2(25, 36, 40, 42, 51, 64) 
-*add_state3(26, 37, 41, 43, 52, 65) 
-*add_state2(27, 38, 42, 44, 53, 66) 
-*add_state3(28, 39, 43, 45, 54, 67) 
-*add_state2(29, 40, 44, 46, 55, 68) 
-*add_state3(30, 41, 45, 47, 56, 69) 
-*add_state2(31, 42, 46, 48, 57, 70) 
-*add_state3(32, 43, 47, 49, 58, 71) 
-*add_state2(33, 44, 48, 50, 59, 72) 
-*add_state3(34, 45, 49, 51, 60, 73) 
-*add_state2(35, 46, 50, 52, 61, 74) 
-*add_state3(36, 47, 51, 53, 62, 75) 
-*add_state2(37, 48, 52, 54, 63, 76) 
-*add_state3(38, 49, 53, 55, 64, 77) 
-*add_state2(39, 50, 54, 56, 65, 78) 
-*add_state3(40, 51, 55, 57, 66, 79)
+#xor(-1, xor(16, and(-18, 27), 18), equ(40, 12))
+add_state2(1, 12, 16, 18, 27, 40)
+add_state3(2, 13, 17, 19, 28, 41) 
+add_state2(3, 14, 18, 20, 29, 42) 
+add_state3(4, 15, 19, 21, 30, 43) 
+add_state2(5, 16, 20, 22, 31, 44) 
+add_state3(6, 17, 21, 23, 32, 45) 
+add_state2(7, 18, 22, 24, 33, 46) 
+add_state3(8, 19, 23, 25, 34, 47) 
+add_state2(9, 20, 24, 26, 35, 48) 
+add_state3(10, 21, 25, 27, 36, 49) 
+add_state2(11, 22, 26, 28, 37, 50) 
+add_state3(12, 23, 27, 29, 38, 51) 
+add_state2(13, 24, 28, 30, 39, 52) 
+add_state3(14, 25, 29, 31, 40, 53) 
+add_state2(15, 26, 30, 32, 41, 54) 
+add_state3(16, 27, 31, 33, 42, 55) 
+add_state2(17, 28, 32, 34, 43, 56) 
+add_state3(18, 29, 33, 35, 44, 57) 
+add_state2(19, 30, 34, 36, 45, 58) 
+add_state3(20, 31, 35, 37, 46, 59) 
+add_state2(21, 32, 36, 38, 47, 60) 
+add_state3(22, 33, 37, 39, 48, 61)
+add_state2(23, 34, 38, 40, 49, 62) 
+add_state3(24, 35, 39, 41, 50, 63) 
+add_state2(25, 36, 40, 42, 51, 64) 
+add_state3(26, 37, 41, 43, 52, 65) 
+add_state2(27, 38, 42, 44, 53, 66) 
+add_state3(28, 39, 43, 45, 54, 67) 
+add_state2(29, 40, 44, 46, 55, 68) 
+add_state3(30, 41, 45, 47, 56, 69) 
+add_state2(31, 42, 46, 48, 57, 70) 
+add_state3(32, 43, 47, 49, 58, 71) 
+add_state2(33, 44, 48, 50, 59, 72) 
+add_state3(34, 45, 49, 51, 60, 73) 
+add_state2(35, 46, 50, 52, 61, 74) 
+add_state3(36, 47, 51, 53, 62, 75) 
+add_state2(37, 48, 52, 54, 63, 76) 
+add_state3(38, 49, 53, 55, 64, 77) 
+add_state2(39, 50, 54, 56, 65, 78) 
+add_state3(40, 51, 55, 57, 66, 79)
diff --git a/tests/longer_tests/slider_80_unsat.ite b/tests/longer_tests/slider_80_unsat.ite
diff --git a/tests/xortest.ite b/tests/xortest.ite
