+++ /dev/null
-#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);
-}
+++ /dev/null
-#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);
-}
+++ /dev/null
-#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
+++ /dev/null
-#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);
-}
--- /dev/null
+#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);
+}
--- /dev/null
+#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
--- /dev/null
+#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);
+}
--- /dev/null
+#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);
+}