Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / Backend / satencoder.cc

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index e053d78514f0b3d2b33868837aa2bd5ca97fb1c0..618b8c17c22114177393754313dda6a3c1d8aa5c 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,56 +11,82 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
+#include "tunable.h"
 
-SATEncoder::SATEncoder(CSolver * _solver) :
+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;
+               Edge e = {(Node *) booledgeMap.get(constraint)};
+               return c.isNegated() ? constraintNegate(e) : e;
        }
-       
+
        switch (constraint->type) {
        case ORDERCONST:
-               result=encodeOrderSATEncoder((BooleanOrder *) constraint);
+               result = encodeOrderSATEncoder((BooleanOrder *) constraint);
                break;
        case BOOLEANVAR:
-               result=encodeVarSATEncoder((BooleanVar *) constraint);
+               result = encodeVarSATEncoder((BooleanVar *) constraint);
                break;
        case LOGICOP:
-               result=encodeLogicSATEncoder((BooleanLogic *) constraint);
+               result = encodeLogicSATEncoder((BooleanLogic *) constraint);
                break;
        case PREDICATEOP:
-               result=encodePredicateSATEncoder((BooleanPredicate *) constraint);
+               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) {
@@ -87,14 +113,15 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        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_IFF:
+               ASSERT(constraint->inputs.getSize() == 2);
+               return constraintIFF(cnf, array[0], array[1]);
+       case SATC_OR:
        case SATC_XOR:
-               return constraintXOR(cnf, array[0], array[1]);
        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);
@@ -129,9 +156,9 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 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. */
        switch ( element->type) {
        case ELEMFUNCRETURN:
@@ -149,7 +176,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) {
 }
 
 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
-       switch (function->function->type) {
+       switch (function->getFunction()->type) {
        case TABLEFUNC:
                encodeTableElementFunctionSATEncoder(function);
                break;
@@ -162,7 +189,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
-       switch (getElementFunctionEncoding(function)->type) {
+       switch (function->getElementFunctionEncoding()->type) {
        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;