Merging with branch master and fixing bugs

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index a9a4f624820e6f64adfdb145750c4378399a62b4..db42f316afaff7d19da8dbe610f822df5c53f84f 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,12 +11,12 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "orderdecompose.h"
+#include "analyzer.h"
 #include "autotuner.h"
 
 CSolver::CSolver() :
        unsat(false),
-       tuner(new DefaultTuner()),
+       tuner(NULL),
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
@@ -61,7 +61,6 @@ CSolver::~CSolver() {
        }
 
        delete satEncoder;
-       delete tuner;
 }
 
 CSolver *CSolver::clone() {
@@ -70,7 +69,7 @@ CSolver *CSolver::clone() {
        HSIteratorBoolean *it = getConstraints();
        while (it->hasNext()) {
                Boolean *b = it->next();
-               b->clone(copy, &map);
+               copy->addConstraint(b->clone(copy, &map));
        }
        delete it;
        return copy;
@@ -113,16 +112,31 @@ Element *CSolver::getElementVar(Set *set) {
 Element *CSolver::getElementConst(VarType type, uint64_t value) {
        uint64_t array[] = {value};
        Set *set = new Set(type, array, 1);
-       allSets.push(set);
        Element *element = new ElementConst(value, type, set);
-       allElements.push(element);
-       return element;
+       Element *e = elemMap.get(element);
+       if (e == NULL) {
+               allSets.push(set);
+               allElements.push(element);
+               elemMap.put(element, element);
+               return element;
+       } else {
+               delete set;
+               delete element;
+               return e;
+       }
 }
 
-Boolean *CSolver::getBooleanVar(VarType type) {
-       Boolean *boolean = new BooleanVar(type);
-       allBooleans.push(boolean);
-       return boolean;
+Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
+       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
+       Element *e = elemMap.get(element);
+       if (e == NULL) {
+               allElements.push(element);
+               elemMap.put(element, element);
+               return element;
+       } else {
+               delete element;
+               return e;
+       }
 }
 
 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
@@ -163,10 +177,10 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
        return function;
 }
 
-Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
-       Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
-       allElements.push(element);
-       return element;
+Boolean *CSolver::getBooleanVar(VarType type) {
+       Boolean *boolean = new BooleanVar(type);
+       allBooleans.push(boolean);
+       return boolean;
 }
 
 Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
@@ -175,14 +189,34 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu
 
 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
        BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-       allBooleans.push(boolean);
-       return boolean;
+       Boolean * b = boolMap.get(boolean);
+       if (b == NULL) {
+               boolMap.put(boolean, boolean);
+               allBooleans.push(boolean);
+               return boolean;
+       } else {
+               delete boolean;
+               return b;
+       }
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean *boolean = new BooleanLogic(this, op, array, asize);
-       allBooleans.push(boolean);
-       return boolean;
+       Boolean *b = boolMap.get(boolean);
+       if (b == NULL) {
+               boolMap.put(boolean, boolean);
+               allBooleans.push(boolean);
+               return boolean;         
+       } else {
+               delete boolean;
+               return b;
+       }
+}
+
+Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+       Boolean *constraint = new BooleanOrder(order, first, second);
+       allBooleans.push(constraint);
+       return constraint;
 }
 
 void CSolver::addConstraint(Boolean *constraint) {
@@ -195,26 +229,30 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
-Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
-       Boolean *constraint = new BooleanOrder(order, first, second);
-       allBooleans.push(constraint);
-       return constraint;
-}
-
 int CSolver::startEncoding() {
+       bool deleteTuner = false;
+       if (tuner == NULL) {
+               tuner = new DefaultTuner();
+               deleteTuner = true;
+       }
+               
        long long startTime = getTimeNano();
        computePolarities(this);
        orderAnalysis(this);
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
-       int result = satEncoder->solve();
+       int result = unsat ? IS_UNSAT : satEncoder->solve();
        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
+       if (deleteTuner) {
+               delete tuner;
+               tuner = NULL;
+       }
        return result;
 }
 
 uint64_t CSolver::getElementValue(Element *element) {
-       switch (GETELEMENTTYPE(element)) {
+       switch (element->type) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
@@ -226,7 +264,7 @@ uint64_t CSolver::getElementValue(Element *element) {
 }
 
 bool CSolver::getBooleanValue(Boolean *boolean) {
-       switch (GETBOOLEANTYPE(boolean)) {
+       switch (boolean->type) {
        case BOOLEANVAR:
                return getBooleanVariableValueSATTranslator(this, boolean);
        default:
@@ -247,4 +285,5 @@ void CSolver::autoTune(uint budget) {
        AutoTuner * autotuner=new AutoTuner(budget);
        autotuner->addProblem(this);
        autotuner->tune();
+       delete autotuner;
 }