X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FTest%2Ffuncencodingtest.cc;h=72a0a8389a2540069d6e00ac8a705c67f8379cb0;hp=b842ff02117e8f3c496a92bb88a43a2fa6645404;hb=806a79424211fba5d68b6b802a6ceea2db47196f;hpb=0ce5a25b09b4b54cd763758388075b1f61ccefcb

diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc
index b842ff0..72a0a83 100644
--- a/src/Test/funcencodingtest.cc
+++ b/src/Test/funcencodingtest.cc
@@ -31,10 +31,10 @@ int main(int numargs, char **argv) {
 	Element *e1 = solver->getElementVar(s1);
 	Element *e2 = solver->getElementVar(s2);
 	Element *e7 = solver->getElementVar(s5);
-	Boolean *overflow = solver->getBooleanVar(2);
+	BooleanEdge overflow = solver->getBooleanVar(2);
 	Set *d1[] = {s1, s2};
 	//change the overflow flag
-	Function *f1 = solver->createFunctionOperator(SUB, d1, 2, s2, IGNORE);
+	Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE);
 	Element *in1[] = {e1, e2};
 	Element *e3 = solver->applyFunction(f1, in1, 2, overflow);
 	Table *t1 = solver->createTable(d1, 2, s3);
@@ -42,7 +42,7 @@ int main(int numargs, char **argv) {
 	uint64_t row2[] = {6, 4};
 	solver->addTableEntry(t1, row1, 2, 3);
 	solver->addTableEntry(t1, row2, 2, 1);
-	Function *f2 = solver->completeTable(t1, IGNOREBEHAVIOR);
+	Function *f2 = solver->completeTable(t1, SATC_IGNOREBEHAVIOR);
 	Element *e4 = solver->applyFunction(f2, in1, 2, overflow);
 
 	Set *d2[] = {s1};
@@ -50,7 +50,7 @@ int main(int numargs, char **argv) {
 	Table *t2 = solver->createTable(d2, 1, s1);
 	uint64_t row3[] = {6};
 	solver->addTableEntry(t2, row3, 1, 6);
-	Function *f3 = solver->completeTable(t2, IGNOREBEHAVIOR);
+	Function *f3 = solver->completeTable(t2, SATC_IGNOREBEHAVIOR);
 	Element *e5 = solver->applyFunction(f3, in2, 1, overflow);
 
 	Set *d3[] = {s2, s3, s1};
@@ -64,16 +64,17 @@ int main(int numargs, char **argv) {
 	solver->addTableEntry(t3, row5, 3, 1);
 	solver->addTableEntry(t3, row6, 3, 2);
 	solver->addTableEntry(t3, row7, 3, 1);
-	Function *f4 = solver->completeTable(t3, IGNOREBEHAVIOR);
+	Function *f4 = solver->completeTable(t3, SATC_IGNOREBEHAVIOR);
 	Element *e6 = solver->applyFunction(f4, in3, 3, overflow);
 
 	Set *deq[] = {s5,s4};
-	Predicate *gt = solver->createPredicateOperator(GT, deq, 2);
+	Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2);
 	Element *inputs2 [] = {e7, e6};
-	Boolean *pred = solver->applyPredicate(gt, inputs2, 2);
+	BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);
 	solver->addConstraint(pred);
+	solver->serialize();
 
-	if (solver->startEncoding() == 1)
+	if (solver->solve() == 1)
 		printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
 					 solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));
 	else