From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 00:21:55 +0000 (-0700)
Subject: test file name convention ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=91a62e5792d982b143ff83203b97edda95ef08b8;p=satune.git

test file name convention ...
---

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
deleted file mode 100644
index e795038..0000000
--- a/src/Test/buildconstraints.c
+++ /dev/null
@@ -1,47 +0,0 @@
-#include "csolver.h"
-
-int main(int numargs, char ** argv) {
-	CSolver * solver=allocCSolver();
-	uint64_t set1[]={0, 1, 2};
-	uint64_t setbigarray[]={0, 1, 2, 3, 4};
-	
-	Set * s=createSet(solver, 0, set1, 3);
-	Set * setbig=createSet(solver, 0, setbigarray, 5);
-	Element * e1=getElementVar(solver, s);
-	Element * e2=getElementVar(solver, s);
-	Set * domain[]={s, s};
-	Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
-	Element * inputs[]={e1, e2};
-	Boolean * b=applyPredicate(solver, equals, inputs, 2);
-	addConstraint(solver, b);
-
-	uint64_t set2[] = {2, 3};
-	Set* rangef1 = createSet(solver, 1, set2, 2);
-	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE);
-	
-	Table* table = createTable(solver, domain, 2, s);
-	uint64_t row1[] = {0, 1};
-	uint64_t row2[] = {1, 1};
-	uint64_t row3[] = {2, 1};
-	uint64_t row4[] = {2, 2};
-	addTableEntry(solver, table, row1, 2, 0);
-	addTableEntry(solver, table, row2, 2, 0);
-	addTableEntry(solver, table, row3, 2, 2);
-	addTableEntry(solver, table, row4, 2, 2);
-	Function * f2 = completeTable(solver, table); //its range would be as same as s
-	
-	Boolean* overflow = getBooleanVar(solver , 2);
-	Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
-	Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
-	Set* domain2[] = {s,rangef1};
-	Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
-	Element* inputs2 [] = {e4, e3};
-	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
-	addConstraint(solver, pred);
-	
-	if (startEncoding(solver)==1)
-		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
-	else
-		printf("UNSAT\n");
-	deleteSolver(solver);
-}
diff --git a/src/Test/elemequalityunsat.c b/src/Test/elemequalityunsat.c
deleted file mode 100644
index 1b6addb..0000000
--- a/src/Test/elemequalityunsat.c
+++ /dev/null
@@ -1,22 +0,0 @@
-#include "csolver.h"
-
-int main(int numargs, char ** argv) {
-	CSolver * solver=allocCSolver();
-	uint64_t set1[]={0, 1, 2};
-	uint64_t set2[]={3, 4};
-	Set * s1=createSet(solver, 0, set1, 3);
-	Set * s2=createSet(solver, 0, set2, 2);
-	Element * e1=getElementVar(solver, s1);
-	Element * e2=getElementVar(solver, s2);
-	Set * domain[]={s1, s2};
-	Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
-	Element * inputs[]={e1, e2};
-	Boolean *b=applyPredicate(solver, equals, inputs, 2);
-	addConstraint(solver, b);
-	
-	if (startEncoding(solver)==1)
-		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
-	else
-		printf("UNSAT\n");
-	deleteSolver(solver);
-}
diff --git a/src/Test/elemlt.c b/src/Test/elemlt.c
deleted file mode 100644
index e9ddda1..0000000
--- a/src/Test/elemlt.c
+++ /dev/null
@@ -1,21 +0,0 @@
-#include "csolver.h"
-
-int main(int numargs, char ** argv){
-	CSolver *solver=allocCSolver();
-	uint64_t set1[]={0, 1, 2};
-	uint64_t set3[]={1, 3, 4, 5};
-	Set * s1=createSet(solver, 0, set1, 3);
-	Set * s3=createSet(solver, 0, set3, 4);
-	Element * e1=getElementVar(solver, s1);
-	Element * e3=getElementVar(solver, s3);
-	Set * domain2[]={s1, s3};
-	Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
-	Element * inputs2[]={e1, e3};
-	Boolean *b=applyPredicate(solver, lt, inputs2, 2);
-	addConstraint(solver, b);
-	if (startEncoding(solver)==1)
-		printf("e1=%llu e3=%llu\n", getElementValue(solver,e1), getElementValue(solver, e3));
-	else
-		printf("UNSAT\n");
-	deleteSolver(solver);
-}
\ No newline at end of file
diff --git a/src/Test/funcencoding.c b/src/Test/funcencoding.c
deleted file mode 100644
index 0dacef0..0000000
--- a/src/Test/funcencoding.c
+++ /dev/null
@@ -1,66 +0,0 @@
-#include "csolver.h"
-
-int main(int numargs, char ** argv) {
-	CSolver * solver=allocCSolver();
-	uint64_t set1[]={6};
-	uint64_t set2[]={4, 2};
-	uint64_t set3[]={3, 1};
-	uint64_t set4[]={2, 3, 1};
-	uint64_t set5[]={2, 1, 0};	
-	Set * s1=createSet(solver, 0, set1, 1);
-	Set * s2=createSet(solver, 0, set2, 2);
-	Set * s3=createSet(solver, 0, set3, 2);
-	Set * s4=createSet(solver, 0, set4, 3);
-	Set * s5=createSet(solver, 0, set5, 3);
-	Element * e1=getElementVar(solver, s1);
-	Element * e2=getElementVar(solver, s2);
-	Element * e7=getElementVar(solver, s5);
-	Boolean* overflow = getBooleanVar(solver , 2);
-	Set * d1[]={s1, s2};
-	//change the overflow flag
-	Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
-	Element * in1[]={e1, e2};
-	Element * e3 = applyFunction(solver, f1, in1, 2, overflow);
-	Table* t1 = createTable(solver, d1, 2, s3);
-	uint64_t row1[] = {6, 2};
-	uint64_t row2[] = {6, 4};
-	addTableEntry(solver, t1, row1, 2, 3);
-	addTableEntry(solver, t1, row2, 2, 1);
-	Function * f2 = completeTable(solver, t1);	
-	Element * e4 = applyFunction(solver, f2, in1, 2, overflow);
-	
-	Set *d2[] = {s1};
-	Element *in2[]={e1};
-	Table* t2 = createTable(solver, d2, 1, s1);
-	uint64_t row3[] = {6};
-	addTableEntry(solver, t2, row3, 1, 6);
-	Function * f3 = completeTable(solver, t2);	
-	Element * e5 = applyFunction(solver, f3, in2, 1, overflow);
-	
-	Set *d3[] = {s2, s3, s1};
-	Element *in3[]={e3, e4, e5};
-	Table* t3 = createTable(solver, d3, 3, s4);
-	uint64_t row4[] = {4, 3, 6};
-	uint64_t row5[] = {2, 1, 6};
-	uint64_t row6[] = {2, 3, 6};
-	uint64_t row7[] = {4, 1, 6};
-	addTableEntry(solver, t3, row4, 3, 3);
-	addTableEntry(solver, t3, row5, 3, 1);
-	addTableEntry(solver, t3, row6, 3, 2);
-	addTableEntry(solver, t3, row7, 3, 1);
-	Function * f4 = completeTable(solver, t3);	
-	Element * e6 = applyFunction(solver, f4, in3, 3, overflow);
-	
-	Set* deq[] = {s5,s4};
-	Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
-	Element* inputs2 [] = {e7, e6};
-	Boolean* pred = applyPredicate(solver, gt, inputs2, 2);
-	addConstraint(solver, pred);
-	
-	if (startEncoding(solver)==1)
-		printf("e1=%llu e2=%llu e7=%llu\n", 
-			 getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));
-	else
-		printf("UNSAT\n");
-	deleteSolver(solver);
-}
diff --git a/src/Test/testbuildconstraints.c b/src/Test/testbuildconstraints.c
new file mode 100644
index 0000000..e795038
--- /dev/null
+++ b/src/Test/testbuildconstraints.c
@@ -0,0 +1,47 @@
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+	CSolver * solver=allocCSolver();
+	uint64_t set1[]={0, 1, 2};
+	uint64_t setbigarray[]={0, 1, 2, 3, 4};
+	
+	Set * s=createSet(solver, 0, set1, 3);
+	Set * setbig=createSet(solver, 0, setbigarray, 5);
+	Element * e1=getElementVar(solver, s);
+	Element * e2=getElementVar(solver, s);
+	Set * domain[]={s, s};
+	Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
+	Element * inputs[]={e1, e2};
+	Boolean * b=applyPredicate(solver, equals, inputs, 2);
+	addConstraint(solver, b);
+
+	uint64_t set2[] = {2, 3};
+	Set* rangef1 = createSet(solver, 1, set2, 2);
+	Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE);
+	
+	Table* table = createTable(solver, domain, 2, s);
+	uint64_t row1[] = {0, 1};
+	uint64_t row2[] = {1, 1};
+	uint64_t row3[] = {2, 1};
+	uint64_t row4[] = {2, 2};
+	addTableEntry(solver, table, row1, 2, 0);
+	addTableEntry(solver, table, row2, 2, 0);
+	addTableEntry(solver, table, row3, 2, 2);
+	addTableEntry(solver, table, row4, 2, 2);
+	Function * f2 = completeTable(solver, table); //its range would be as same as s
+	
+	Boolean* overflow = getBooleanVar(solver , 2);
+	Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
+	Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
+	Set* domain2[] = {s,rangef1};
+	Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
+	Element* inputs2 [] = {e4, e3};
+	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
+	addConstraint(solver, pred);
+	
+	if (startEncoding(solver)==1)
+		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+	else
+		printf("UNSAT\n");
+	deleteSolver(solver);
+}
diff --git a/src/Test/testelementlt.c b/src/Test/testelementlt.c
new file mode 100644
index 0000000..e9ddda1
--- /dev/null
+++ b/src/Test/testelementlt.c
@@ -0,0 +1,21 @@
+#include "csolver.h"
+
+int main(int numargs, char ** argv){
+	CSolver *solver=allocCSolver();
+	uint64_t set1[]={0, 1, 2};
+	uint64_t set3[]={1, 3, 4, 5};
+	Set * s1=createSet(solver, 0, set1, 3);
+	Set * s3=createSet(solver, 0, set3, 4);
+	Element * e1=getElementVar(solver, s1);
+	Element * e3=getElementVar(solver, s3);
+	Set * domain2[]={s1, s3};
+	Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
+	Element * inputs2[]={e1, e3};
+	Boolean *b=applyPredicate(solver, lt, inputs2, 2);
+	addConstraint(solver, b);
+	if (startEncoding(solver)==1)
+		printf("e1=%llu e3=%llu\n", getElementValue(solver,e1), getElementValue(solver, e3));
+	else
+		printf("UNSAT\n");
+	deleteSolver(solver);
+}
\ No newline at end of file
diff --git a/src/Test/testelemequalityunsat.c b/src/Test/testelemequalityunsat.c
new file mode 100644
index 0000000..1b6addb
--- /dev/null
+++ b/src/Test/testelemequalityunsat.c
@@ -0,0 +1,22 @@
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+	CSolver * solver=allocCSolver();
+	uint64_t set1[]={0, 1, 2};
+	uint64_t set2[]={3, 4};
+	Set * s1=createSet(solver, 0, set1, 3);
+	Set * s2=createSet(solver, 0, set2, 2);
+	Element * e1=getElementVar(solver, s1);
+	Element * e2=getElementVar(solver, s2);
+	Set * domain[]={s1, s2};
+	Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
+	Element * inputs[]={e1, e2};
+	Boolean *b=applyPredicate(solver, equals, inputs, 2);
+	addConstraint(solver, b);
+	
+	if (startEncoding(solver)==1)
+		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+	else
+		printf("UNSAT\n");
+	deleteSolver(solver);
+}
diff --git a/src/Test/testfuncencoding.c b/src/Test/testfuncencoding.c
new file mode 100644
index 0000000..0dacef0
--- /dev/null
+++ b/src/Test/testfuncencoding.c
@@ -0,0 +1,66 @@
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+	CSolver * solver=allocCSolver();
+	uint64_t set1[]={6};
+	uint64_t set2[]={4, 2};
+	uint64_t set3[]={3, 1};
+	uint64_t set4[]={2, 3, 1};
+	uint64_t set5[]={2, 1, 0};	
+	Set * s1=createSet(solver, 0, set1, 1);
+	Set * s2=createSet(solver, 0, set2, 2);
+	Set * s3=createSet(solver, 0, set3, 2);
+	Set * s4=createSet(solver, 0, set4, 3);
+	Set * s5=createSet(solver, 0, set5, 3);
+	Element * e1=getElementVar(solver, s1);
+	Element * e2=getElementVar(solver, s2);
+	Element * e7=getElementVar(solver, s5);
+	Boolean* overflow = getBooleanVar(solver , 2);
+	Set * d1[]={s1, s2};
+	//change the overflow flag
+	Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE);
+	Element * in1[]={e1, e2};
+	Element * e3 = applyFunction(solver, f1, in1, 2, overflow);
+	Table* t1 = createTable(solver, d1, 2, s3);
+	uint64_t row1[] = {6, 2};
+	uint64_t row2[] = {6, 4};
+	addTableEntry(solver, t1, row1, 2, 3);
+	addTableEntry(solver, t1, row2, 2, 1);
+	Function * f2 = completeTable(solver, t1);	
+	Element * e4 = applyFunction(solver, f2, in1, 2, overflow);
+	
+	Set *d2[] = {s1};
+	Element *in2[]={e1};
+	Table* t2 = createTable(solver, d2, 1, s1);
+	uint64_t row3[] = {6};
+	addTableEntry(solver, t2, row3, 1, 6);
+	Function * f3 = completeTable(solver, t2);	
+	Element * e5 = applyFunction(solver, f3, in2, 1, overflow);
+	
+	Set *d3[] = {s2, s3, s1};
+	Element *in3[]={e3, e4, e5};
+	Table* t3 = createTable(solver, d3, 3, s4);
+	uint64_t row4[] = {4, 3, 6};
+	uint64_t row5[] = {2, 1, 6};
+	uint64_t row6[] = {2, 3, 6};
+	uint64_t row7[] = {4, 1, 6};
+	addTableEntry(solver, t3, row4, 3, 3);
+	addTableEntry(solver, t3, row5, 3, 1);
+	addTableEntry(solver, t3, row6, 3, 2);
+	addTableEntry(solver, t3, row7, 3, 1);
+	Function * f4 = completeTable(solver, t3);	
+	Element * e6 = applyFunction(solver, f4, in3, 3, overflow);
+	
+	Set* deq[] = {s5,s4};
+	Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
+	Element* inputs2 [] = {e7, e6};
+	Boolean* pred = applyPredicate(solver, gt, inputs2, 2);
+	addConstraint(solver, pred);
+	
+	if (startEncoding(solver)==1)
+		printf("e1=%llu e2=%llu e7=%llu\n", 
+			 getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));
+	else
+		printf("UNSAT\n");
+	deleteSolver(solver);
+}