* Result: b1=1 b2=0 b3=0 b4=0
*/
int main(int numargs, char **argv) {
- CSolver *solver = allocCSolver();
- Boolean *b1 = getBooleanVar(solver, 0);
- Boolean *b2 = getBooleanVar(solver, 0);
- Boolean *b3 = getBooleanVar(solver, 0);
- Boolean *b4 = getBooleanVar(solver, 0);
- //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES
- Boolean * barray1[]={b1,b2};
- Boolean *andb1b2 = applyLogicalOperation(solver, L_AND, barray1, 2);
- Boolean * barray2[]={andb1b2, b3};
- Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, barray2, 2);
- addConstraint(solver, imply);
- Boolean * barray3[] ={b3};
- Boolean *notb3 = applyLogicalOperation(solver, L_NOT, barray3, 1);
- Boolean * barray4[] ={notb3, b4};
- addConstraint(solver, applyLogicalOperation(solver, L_OR, barray4, 2));
- Boolean * barray5[] ={b1, b4};
- addConstraint(solver, applyLogicalOperation(solver, L_XOR, barray5, 2));
- if (startEncoding(solver) == 1)
+ CSolver *solver = new CSolver();
+ Boolean *b1 = solver->getBooleanVar(0);
+ Boolean *b2 = solver->getBooleanVar(0);
+ Boolean *b3 = solver->getBooleanVar(0);
+ Boolean *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);
+ solver->addConstraint(imply);
+ Boolean *barray3[] = {b3};
+ Boolean *notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
+ Boolean *barray4[] = {notb3, b4};
+ solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
+ Boolean *barray5[] = {b1, b4};
+ solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
+ if (solver->startEncoding() == 1)
printf("b1=%d b2=%d b3=%d b4=%d\n",
- getBooleanValue(solver,b1), getBooleanValue(solver, b2),
- getBooleanValue(solver, b3), getBooleanValue(solver, b4));
+ solver->getBooleanValue(b1), solver->getBooleanValue(b2),
+ solver->getBooleanValue(b3), solver->getBooleanValue(b4));
else
printf("UNSAT\n");
- deleteSolver(solver);
+ delete solver;
}