#include "order.h"
#include "predicate.h"
#include "set.h"
+#include "tunable.h"
SATEncoder::SATEncoder(CSolver *_solver) :
cnf(createCNF()),
- solver(_solver) {
+ solver(_solver),
+ vector(allocDefVectorEdge()) {
}
SATEncoder::~SATEncoder() {
deleteCNF(cnf);
+ deleteVectorEdge(vector);
}
-int SATEncoder::solve() {
+void SATEncoder::resetSATEncoder() {
+ resetCNF(cnf);
+ booledgeMap.reset();
+}
+
+int SATEncoder::solve(long timeout) {
+ cnf->solver->timeout = timeout;
return solveCNF(cnf);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
- SetIteratorBoolean *iterator = csolver->getConstraints();
+ if (csolver->isUnSAT()) {
+ return;
+ }
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
- Boolean *constraint = iterator->next();
+ BooleanEdge constraint = iterator->next();
Edge c = encodeConstraintSATEncoder(constraint);
addConstraintCNF(cnf, c);
}
delete iterator;
}
-Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
+Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
Edge result;
+ Boolean *constraint = c.getBoolean();
+
if (booledgeMap.contains(constraint)) {
Edge e = {(Node *) booledgeMap.get(constraint)};
- return e;
+ return c.isNegated() ? constraintNegate(e) : e;
}
switch (constraint->type) {
case PREDICATEOP:
result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
break;
+ case BOOLCONST:
+ result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
+ break;
default:
model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
exit(-1);
}
- booledgeMap.put(constraint, result.node_ptr);
- return result;
+ Polarity p = constraint->polarity;
+ uint pSize = constraint->parents.getSize();
+
+ if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
+ Edge e = getNewVarSATEncoder();
+ generateProxy(cnf, result, e, p);
+ booledgeMap.put(constraint, e.node_ptr);
+ result = e;
+ }
+
+ return c.isNegated() ? constraintNegate(result) : result;
}
void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
switch (constraint->op) {
case SATC_AND:
return constraintAND(cnf, constraint->inputs.getSize(), array);
- case SATC_OR:
- return constraintOR(cnf, constraint->inputs.getSize(), array);
case SATC_NOT:
return constraintNegate(array[0]);
- case SATC_XOR:
- return constraintXOR(cnf, array[0], array[1]);
case SATC_IFF:
+ ASSERT(constraint->inputs.getSize() == 2);
return constraintIFF(cnf, array[0], array[1]);
+ case SATC_OR:
+ case SATC_XOR:
case SATC_IMPLIES:
- return constraintIMPLIES(cnf, array[0], array[1]);
+ //Don't handle, translate these away...
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
exit(-1);
void SATEncoder::encodeElementSATEncoder(Element *element) {
/* Check to see if we have already encoded this element. */
- if (getElementEncoding(element)->variables != NULL)
+ if (element->getElementEncoding()->variables != NULL)
return;
/* Need to encode. */
}
void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
- switch (function->function->type) {
+ switch (function->getFunction()->type) {
case TABLEFUNC:
encodeTableElementFunctionSATEncoder(function);
break;
}
void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
- switch (getElementFunctionEncoding(function)->type) {
+ switch (function->getElementFunctionEncoding()->type) {
case ENUMERATEIMPLICATIONS:
encodeEnumTableElemFunctionSATEncoder(function);
break;