Set *domain[] = {s, s};
Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
Element *inputs[] = {e1, e2};
- Boolean *b = solver->applyPredicate(equals, inputs, 2);
+ BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
solver->addConstraint(b);
uint64_t set2[] = {2, 3};
solver->addTableEntry(table, row3, 2, 2);
solver->addTableEntry(table, row4, 2, 2);
Function *f2 = solver->completeTable(table, SATC_IGNOREBEHAVIOR); //its range would be as same as s
- Boolean *overflow = solver->getBooleanVar(2);
+ BooleanEdge overflow = solver->getBooleanVar(2);
Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
Element *e4 = solver->applyFunction(f2, inputs, 2, overflow);
Set *domain2[] = {s,rangef1};
Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
Element *inputs2 [] = {e4, e3};
- Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
+ BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
solver->addConstraint(pred);
if (solver->solve() == 1)
Set *domain[] = {s1, s2};
Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
Element *inputs[] = {e1, e2};
- Boolean *b = solver->applyPredicate(equals, inputs, 2);
+ BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
solver->addConstraint(b);
if (solver->solve() == 1)
Set *domain[] = {s1, s2};
Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
Element *inputs[] = {e1, e2};
- Boolean *b = solver->applyPredicate(equals, inputs, 2);
+ BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
solver->addConstraint(b);
if (solver->solve() == 1)
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(SATC_SUB, d1, 2, s2, SATC_IGNORE);
Set *deq[] = {s5,s4};
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);
if (solver->solve() == 1)
*/
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);
+ 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
- Boolean *barray1[] = {b1,b2};
- Boolean *andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
- Boolean *barray2[] = {andb1b2, b3};
- Boolean *imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);
+ 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(SATC_NOT, barray3, 1);
- Boolean *barray4[] = {notb3, b4};
+ BooleanEdge barray3[] = {b3};
+ BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
+ BooleanEdge barray4[] = {notb3, b4};
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
- Boolean *barray5[] = {b1, b4};
+ BooleanEdge barray5[] = {b1, b4};
solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
if (solver->solve() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
Set *domain2[] = {s1, s3};
Predicate *lt = solver->createPredicateOperator(SATC_LT, domain2, 2);
Element *inputs2[] = {e1, e2};
- Boolean *b = solver->applyPredicate(lt, inputs2, 2);
+ BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);
solver->addConstraint(b);
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
Set *s = solver->createSet(0, set1, 8);
Order *order = solver->createOrder(SATC_TOTAL, s);
- Boolean *o12 = solver->orderConstraint(order, 1, 2);
- Boolean *o13 = solver->orderConstraint(order, 1, 3);
- Boolean *o24 = solver->orderConstraint(order, 2, 4);
- Boolean *o34 = solver->orderConstraint(order, 3, 4);
- Boolean *o41 = solver->orderConstraint(order, 4, 1);
- Boolean *o57 = solver->orderConstraint(order, 5, 7);
- Boolean *o76 = solver->orderConstraint(order, 7, 6);
- Boolean *o65 = solver->orderConstraint(order, 6, 5);
- Boolean *o58 = solver->orderConstraint(order, 5, 8);
- Boolean *o81 = solver->orderConstraint(order, 8, 1);
-
- Boolean *array1[] = {o12, o13, o24, o34};
+ BooleanEdge o12 = solver->orderConstraint(order, 1, 2);
+ BooleanEdge o13 = solver->orderConstraint(order, 1, 3);
+ BooleanEdge o24 = solver->orderConstraint(order, 2, 4);
+ BooleanEdge o34 = solver->orderConstraint(order, 3, 4);
+ BooleanEdge o41 = solver->orderConstraint(order, 4, 1);
+ BooleanEdge o57 = solver->orderConstraint(order, 5, 7);
+ BooleanEdge o76 = solver->orderConstraint(order, 7, 6);
+ BooleanEdge o65 = solver->orderConstraint(order, 6, 5);
+ BooleanEdge o58 = solver->orderConstraint(order, 5, 8);
+ BooleanEdge o81 = solver->orderConstraint(order, 8, 1);
+
+ BooleanEdge array1[] = {o12, o13, o24, o34};
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );
- Boolean *array2[] = {o41, o57};
-
- Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
- Boolean *array3[] = {o34};
- Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
- Boolean *array4[] = {o24};
- Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
- Boolean *array5[] = {o34n, o24n};
- Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
- Boolean *array6[] = {b1, b2};
+ BooleanEdge array2[] = {o41, o57};
+
+ BooleanEdge b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
+ BooleanEdge array3[] = {o34};
+ BooleanEdge o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
+ BooleanEdge array4[] = {o24};
+ BooleanEdge o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
+ BooleanEdge array5[] = {o34n, o24n};
+ BooleanEdge b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
+ BooleanEdge array6[] = {b1, b2};
solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
- Boolean *array7[] = {o12, o13};
+ BooleanEdge array7[] = {o12, o13};
solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
- Boolean *array8[] = {o76, o65};
+ BooleanEdge array8[] = {o76, o65};
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
- Boolean *array9[] = {o76, o65};
- Boolean *b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
- Boolean *array10[] = {o57};
- Boolean *o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
- Boolean *array11[] = {b3, o57n};
+ BooleanEdge array9[] = {o76, o65};
+ BooleanEdge b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
+ BooleanEdge array10[] = {o57};
+ BooleanEdge o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
+ BooleanEdge array11[] = {b3, o57n};
solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
- Boolean *array12[] = {o58, o81};
+ BooleanEdge array12[] = {o58, o81};
solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
/* if (solver->solve() == 1)
uint64_t set1[] = {5, 1, 4};
Set *s = solver->createSet(0, set1, 3);
Order *order = solver->createOrder(SATC_TOTAL, s);
- Boolean *b1 = solver->orderConstraint(order, 5, 1);
- Boolean *b2 = solver->orderConstraint(order, 1, 4);
+ BooleanEdge b1 = solver->orderConstraint(order, 5, 1);
+ BooleanEdge b2 = solver->orderConstraint(order, 1, 4);
solver->addConstraint(b1);
solver->addConstraint(b2);
if (solver->solve() == 1)
Element *e1 = solver->getElementVar(s1);
Element *e2 = solver->getElementVar(s2);
Element *e4 = solver->getElementVar(s3);
- Boolean *overflow = solver->getBooleanVar(2);
+ BooleanEdge overflow = solver->getBooleanVar(2);
Set *d1[] = {s1, s2};
//change the overflow flag
Table *t1 = solver->createTable(d1, 2, s2);
Set *deq[] = {s3,s2};
Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2);
Element *inputs2 [] = {e4, e3};
- Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
+ BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2);
solver->addConstraint(pred);
if (solver->solve() == 1)
solver->addTableEntry(t1, row5, 3, false);
solver->addTableEntry(t1, row6, 3, true);
Predicate *p1 = solver->createPredicateTable(t1, SATC_FLAGIFFUNDEFINED);
- Boolean *undef = solver->getBooleanVar(2);
+ BooleanEdge undef = solver->getBooleanVar(2);
Element *tmparray[] = {e1, e2, e3};
- Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
+ BooleanEdge b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
solver->addConstraint(b1);
Set *deq[] = {s3,s2};
Predicate *gte = solver->createPredicateOperator(SATC_GTE, deq, 2);
Element *inputs2 [] = {e3, e2};
- Boolean *pred = solver->applyPredicate(gte, inputs2, 2);
+ BooleanEdge pred = solver->applyPredicate(gte, inputs2, 2);
solver->addConstraint(pred);
Set *d1[] = {s1, s2};
Predicate *eq = solver->createPredicateOperator(SATC_EQUALS, d1, 2);
Element *tmparray2[] = {e1, e2};
- Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
+ BooleanEdge pred2 = solver->applyPredicate(eq, tmparray2, 2);
solver->addConstraint(pred2);
if (solver->solve() == 1)