}
Edge result=constraintOR(This->cnf, size, constraints);
- return generateNegation ? result: constraintNegate(result);
+ return generateNegation ? constraintNegate(result) : result;
}
Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
Element * elem = getArrayElement(&constraint->inputs, i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
- pushVectorEdge(clauses, constraintAND(This->cnf, numDomains, carray));
+ Edge term=constraintAND(This->cnf, numDomains, carray);
+ pushVectorEdge(clauses, term);
}
notfinished=false;
Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
deleteVectorEdge(clauses);
- return generateNegation ? cor : constraintNegate(cor);
+ return generateNegation ? constraintNegate(cor) : cor;
}
Element * inputs[]={e1, e2};
Boolean * b=applyPredicate(solver, equals, inputs, 2);
addConstraint(solver, b);
- Order * o=createOrder(solver, TOTAL, s);
- Boolean * oc=orderConstraint(solver, o, 1, 2);
- addConstraint(solver, oc);
-
+
uint64_t set2[] = {2, 3};
Set* rangef1 = createSet(solver, 1, set2, 2);
Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
uint64_t row3[] = {2, 1};
uint64_t row4[] = {1, 2};
addTableEntry(solver, table, row1, 2, 0);
- addTableEntry(solver, table, row2, 2, 1);
+ 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* pred = applyPredicate(solver, equal2, inputs2, 2);
addConstraint(solver, pred);
- startEncoding(solver);
+ if (startEncoding(solver)==1)
+ printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
deleteSolver(solver);
}
return constraint;
}
-void startEncoding(CSolver* This){
+int startEncoding(CSolver* This){
naiveEncodingDecision(This);
SATEncoder* satEncoder = This->satEncoder;
encodeAllSATEncoder(This, satEncoder);
model_print("%d, ", satEncoder->cnf->solver->solution[i]);
}
model_print("\n");
+ return result;
}
uint64_t getElementValue(CSolver* This, Element* element){
Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
/** When everything is done, the client calls this function and then csolver starts to encode*/
-void startEncoding(CSolver*);
+int startEncoding(CSolver*);
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(CSolver*, Element* element);