Adding settings to usedsettings when tuner hits timeout

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 2670e4745a24c0371aaa4db082be7890bec86666..1dfe9eb8ec9cf012f9af880c672e62a9ff95c81b 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -31,6 +31,8 @@
 #include <stdarg.h>
 #include "alloyinterpreter.h"
 #include "smtinterpreter.h"
+#include "mathsatinterpreter.h"
+#include "smtratinterpreter.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -83,8 +85,8 @@ CSolver::~CSolver() {
        for (uint i = 0; i < size; i++) {
                delete allFunctions.get(i);
        }
-       
-       if(interpreter != NULL){
+
+       if (interpreter != NULL) {
                delete interpreter;
        }
 
@@ -317,7 +319,7 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
        allBooleans.push(boolean);
-       if(!booleanVarUsed)
+       if (!booleanVarUsed)
                booleanVarUsed = true;
        return BooleanEdge(boolean);
 }
@@ -395,7 +397,7 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-       if(!useInterpreter()){
+       if (!useInterpreter()) {
                BooleanEdge newarray[asize];
                switch (op) {
                case SATC_NOT: {
@@ -458,7 +460,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                        return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
                }
                }
-       
+
                ASSERT(asize != 0);
                Boolean *boolean = new BooleanLogic(this, op, array, asize);
                Boolean *b = boolMap.get(boolean);
@@ -476,7 +478,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                Boolean *boolean = new BooleanLogic(this, op, array, asize);
                allBooleans.push(boolean);
                return BooleanEdge(boolean);
-       
+
        }
 }
 
@@ -495,7 +497,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                }
        }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       if (!useInterpreter() ){ 
+       if (!useInterpreter() ) {
                Boolean *b = boolMap.get(constraint);
 
                if (b == NULL) {
@@ -532,7 +534,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if(!useInterpreter()){
+       if (!useInterpreter()) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
@@ -570,7 +572,7 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                        replaceBooleanWithTrueNoRemove(constraint);
                        constraint->parents.clear();
                }
-       } else{
+       } else {
                constraints.add(constraint);
                constraint->parents.clear();
        }
@@ -603,6 +605,9 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
+       if (isUnSAT()) {
+               return IS_UNSAT;
+       }
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -610,12 +615,12 @@ int CSolver::solve() {
                deleteTuner = true;
        }
        int result = IS_INDETER;
-       if(useInterpreter()){
+       if (useInterpreter()) {
                interpreter->encode();
                model_print("Problem encoded in Interpreter\n");
                result = interpreter->solve();
                model_print("Problem solved by Interpreter\n");
-       } else{
+       } else {
 
                {
                        SetIteratorOrder *orderit = activeOrders.iterator();
@@ -651,7 +656,7 @@ int CSolver::solve() {
                eg.encode();
 
                naiveEncodingDecision(this);
-       //      eg.validate();
+               //      eg.validate();
 
                VarOrderingOpt bor(this, satEncoder);
                bor.doTransform();
@@ -665,7 +670,7 @@ int CSolver::solve() {
                model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 
                model_print("Is problem UNSAT after encoding: %d\n", unsat);
-               
+
 
                result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
                model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
@@ -680,22 +685,28 @@ int CSolver::solve() {
        return result;
 }
 
-void CSolver::setInterpreter(InterpreterType type){
-       if(interpreter == NULL){
-               switch(type){
-                       case SATUNE:
-                               break;
-                       case ALLOY:{
-                               interpreter = new AlloyInterpreter(this);
-                               break;
-                       }case Z3:{
-                               interpreter = new SMTInterpreter(this);
-                               break;
-                       }
-                       case MATHSAT:
-                       case SMTRAT:
-                       default:
-                               ASSERT(0);
+void CSolver::setInterpreter(InterpreterType type) {
+       if (interpreter == NULL) {
+               switch (type) {
+               case SATUNE:
+                       break;
+               case ALLOY: {
+                       interpreter = new AlloyInterpreter(this);
+                       break;
+               } case Z3: {
+                       interpreter = new SMTInterpreter(this);
+                       break;
+               }
+               case MATHSAT: {
+                       interpreter = new MathSATInterpreter(this);
+                       break;
+               }
+               case SMTRAT: {
+                       interpreter = new SMTRatInterpreter(this);
+                       break;
+               }
+               default:
+                       ASSERT(0);
                }
        }
 }
@@ -718,8 +729,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return useInterpreter()? interpreter->getValue(element):
-                       getElementValueSATTranslator(this, element);
+               return useInterpreter() ? interpreter->getValue(element) :
+                                        getElementValueSATTranslator(this, element);
        default:
                ASSERT(0);
        }
@@ -730,8 +741,8 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) {
        Boolean *boolean = bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
-               return useInterpreter()? interpreter->getBooleanValue(boolean):
-                       getBooleanVariableValueSATTranslator(this, boolean);
+               return useInterpreter() ? interpreter->getBooleanValue(boolean) :
+                                        getBooleanVariableValueSATTranslator(this, boolean);
        default:
                ASSERT(0);
        }