CSolver *solver = new CSolver();
uint64_t set1[] = {5, 1, 4};
Set *s = solver->createSet(0, set1, 3);
- Order *order = solver->createOrder(TOTAL, s);
- Boolean *b1 = solver->orderConstraint(order, 5, 1);
- Boolean *b2 = solver->orderConstraint(order, 1, 4);
+ Order *order = solver->createOrder(SATC_TOTAL, s);
+ BooleanEdge b1 = solver->orderConstraint(order, 5, 1);
+ BooleanEdge b2 = solver->orderConstraint(order, 1, 4);
solver->addConstraint(b1);
solver->addConstraint(b2);
- if (solver->startEncoding() == 1)
+ solver->serialize();
+ if (solver->solve() == 1){
printf("SAT\n");
- else
+ printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+ solver->getOrderConstraintValue(order, 5, 1),
+ solver->getOrderConstraintValue(order, 1, 4),
+ solver->getOrderConstraintValue(order, 5, 4),
+ solver->getOrderConstraintValue(order, 1, 5));
+ } else {
printf("UNSAT\n");
+ }
delete solver;
}