Alloy interpreter

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index fbe0dd082d5070229834d892c2578ecb6af6070b..a8eb999de296c7b58b90af4057deb97e5f1faedb 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -29,14 +29,17 @@
 #include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
+#include "alloyenc.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
        boolFalse(boolTrue.negate()),
        unsat(false),
+       booleanVarUsed(false),
        tuner(NULL),
        elapsedTime(0),
-       satsolverTimeout(NOTIMEOUT)
+       satsolverTimeout(NOTIMEOUT),
+       alloyEncoder(NULL)
 {
        satEncoder = new SATEncoder(this);
 }
@@ -136,6 +139,7 @@ void CSolver::resetSolver() {
        boolTrue = BooleanEdge(new BooleanConst(true));
        boolFalse = boolTrue.negate();
        unsat = false;
+       booleanVarUsed = false;
        elapsedTime = 0;
        tuner = NULL;
        satEncoder->resetSATEncoder();
@@ -308,6 +312,8 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
        allBooleans.push(boolean);
+       if(!booleanVarUsed)
+               booleanVarUsed = true;
        return BooleanEdge(boolean);
 }
 
@@ -634,11 +640,17 @@ int CSolver::solve() {
        model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
-       int 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");
-       time2 = getTimeNano();
-       elapsedTime = time2 - startTime;
-       model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+       int result = IS_INDETER;
+       if(alloyEncoder != NULL){
+               alloyEncoder->encode();
+               result = alloyEncoder->solve();
+       }else{
+               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");
+               time2 = getTimeNano();
+               elapsedTime = time2 - startTime;
+               model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+       }
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
@@ -646,6 +658,10 @@ int CSolver::solve() {
        return result;
 }
 
+void CSolver::setAlloyEncode(){
+       alloyEncoder = new AlloyEnc(this);
+}
+
 void CSolver::printConstraints() {
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -664,7 +680,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return getElementValueSATTranslator(this, element);
+               return alloyEncoder == NULL? getElementValueSATTranslator(this, element):
+                       alloyEncoder->getValue(element);
        default:
                ASSERT(0);
        }