6 int main(int numargs, char **argv) {
7 CSolver *solver = new CSolver();
8 uint64_t set1[] = {3, 1, 2};
9 uint64_t set2[] = {3, 1, 7};
10 Set *s1 = solver->createSet(0, set1, DOMAINSIZE);
11 Set *s2 = solver->createSet(0, set2, DOMAINSIZE);
12 Element *e1 = solver->getElementVar(s1);
13 Element *e2 = solver->getElementVar(s2);
14 Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
15 Element *inputs[] = {e1, e2};
16 BooleanEdge b = solver->applyPredicate(equals, inputs, INPUTSIZE);
17 solver->addConstraint(b);
18 solver->freezeElement(e1);
19 solver->freezeElement(e2);
20 if (solver->solve() == 1){
23 printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2));
24 for(int i=0; i< INPUTSIZE; i++){
25 uint64_t val = solver->getElementValue(inputs[i]);
26 Element *econst = solver->getElementConst(0, val);
27 Element * tmpInputs[] = {inputs[i], econst};
28 BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE);
29 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b));
32 }while(solver->solveIncremental() == 1);
33 printf("After %d runs, there are no more models to find ...\n", run);