X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FTest%2Flogicopstest.cc;h=7b30f80dc3af3168acd2fe9a807dfa83589a2a33;hb=f96c6affc7f990067f4d298d9c989f789933c9ce;hp=df80fa73a50239a8a83d4fb56916917f68f5dbdd;hpb=1bbedcc6a785d0cef637350b1f2f624b290f149f;p=satune.git

diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc
index df80fa7..7b30f80 100644
--- a/src/Test/logicopstest.cc
+++ b/src/Test/logicopstest.cc
@@ -8,23 +8,24 @@
  */
 int main(int numargs, char **argv) {
 	CSolver *solver = new CSolver();
-	Boolean *b1 = solver->getBooleanVar(0);
-	Boolean *b2 = solver->getBooleanVar(0);
-	Boolean *b3 = solver->getBooleanVar(0);
-	Boolean *b4 = solver->getBooleanVar(0);
-	//L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
-	Boolean * barray1[]={b1,b2};
-	Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2);
-	Boolean * barray2[]={andb1b2, b3};
-	Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2);
+	BooleanEdge b1 = solver->getBooleanVar(0);
+	BooleanEdge b2 = solver->getBooleanVar(0);
+	BooleanEdge b3 = solver->getBooleanVar(0);
+	BooleanEdge b4 = solver->getBooleanVar(0);
+	//SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
+	BooleanEdge barray1[] = {b1,b2};
+	BooleanEdge andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
+	BooleanEdge barray2[] = {andb1b2, b3};
+	BooleanEdge imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);
 	solver->addConstraint(imply);
-	Boolean * barray3[] ={b3};
-	Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1);
-	Boolean * barray4[] ={notb3, b4};
-	solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2));
-	Boolean * barray5[] ={b1, b4};
-	solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2));
-	if (solver->startEncoding() == 1)
+	BooleanEdge barray3[] = {b3};
+	BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
+	BooleanEdge barray4[] = {notb3, b4};
+	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
+	BooleanEdge barray5[] = {b1, b4};
+	solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
+	solver->serialize();
+	if (solver->solve() == 1)
 		printf("b1=%d b2=%d b3=%d b4=%d\n",
 					 solver->getBooleanValue(b1), solver->getBooleanValue(b2),
 					 solver->getBooleanValue(b3), solver->getBooleanValue(b4));