Merging + fixing memory bugs

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

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index fdeee9ee8816faf0c812a7696bde8e69b6ba95eb..2e09491a88262617f4c0fbe1bce71508fa5efd53 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -11,33 +11,54 @@
 #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;
+       long long startTime = getTimeNano();
+       finishedClauses(cnf->solver);
+       cnf->encodeTime = getTimeNano() - startTime;
+       if (solver->isIncrementalMode()) {
+               solver->freezeElementsVariables();
+       }
        return solveCNF(cnf);
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+       if (csolver->isUnSAT()) {
+               return;
+       }
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
-               Edge c = encodeConstraintSATEncoder(constraint);
-               addConstraintCNF(cnf, c);
+               if (!csolver->isConstraintEncoded(constraint)) {
+                       Edge c = encodeConstraintSATEncoder(constraint);
+                       addConstraintCNF(cnf, c);
+                       csolver->addEncodedConstraint(constraint);
+               }
        }
        delete iterator;
 }
 
 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        Edge result;
-       Boolean * constraint = c.getBoolean();
+       Boolean *constraint = c.getBoolean();
 
        if (booledgeMap.contains(constraint)) {
                Edge e = {(Node *) booledgeMap.get(constraint)};
@@ -57,11 +78,23 @@ Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        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);
+       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;
 }
 
@@ -92,11 +125,12 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        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:
        case SATC_IMPLIES:
-               //Don't handle, translate these away...
+       //Don't handle, translate these away...
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);