Adding SAT translator

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
new file mode 100644 (file)
index 0000000..a768a4f
--- /dev/null
+++ b/src/Backend/sattranslator.c
@@ -0,0 +1,41 @@
+#include "sattranslator.h"
+#include "element.h"
+#include "csolver.h"
+#include "satencoder.h"
+
+uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
+       uint index=0;
+       for(int i=elemEnc->numVars-1;i>=0;i--) {
+               index=index<<1;
+               if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+                       index |= 1;
+       }
+       ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+       return elemEnc->encodingArray[index];
+}
+uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
+       switch(getElementEncoding(element)->type){
+               case ONEHOT:
+                       ASSERT(0);
+                       break;
+               case UNARY:
+                       ASSERT(0);
+                       break;
+               case BINARYINDEX:
+                       return getElementValueBinaryIndexSATTranslator(This, getElementEncoding(element));
+               case ONEHOTBINARY:
+                       ASSERT(0);
+                       break;
+               case BINARYVAL:
+                       ASSERT(0);
+                       break;
+               default:
+                       ASSERT(0);
+                       break;
+       }
+}
+
+bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
+       int index = getEdgeVar( ((BooleanVar*) boolean)->var );
+       return This->satEncoder->cnf->solver->solution[index] == true;
+}
\ No newline at end of file

diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
new file mode 100644 (file)
index 0000000..5378cdd
--- /dev/null
+++ b/src/Backend/sattranslator.h
@@ -0,0 +1,17 @@
+/* 
+ * File:   sattranslator.h
+ * Author: hamed
+ *
+ * Created on July 11, 2017, 5:27 PM
+ */
+
+#ifndef SATTRANSLATOR_H
+#define SATTRANSLATOR_H
+
+#include "classlist.h"
+
+bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean);
+uint64_t getElementValueSATTranslator(CSolver* This, Element* element);
+
+#endif /* SATTRANSLATOR_H */
+

diff --git a/src/csolver.c b/src/csolver.c
index 40490d535c4ddc7723fa99cd6e7470b029e7cc8a..c12b7ceb8474fb0618db3364bc438d07f35615a8 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -8,6 +8,7 @@
 #include "table.h"
 #include "function.h"
 #include "satencoder.h"
+#include "sattranslator.h"
 
 CSolver * allocCSolver() {
        CSolver * This=(CSolver *) ourmalloc(sizeof(CSolver));
@@ -19,6 +20,7 @@ CSolver * allocCSolver() {
        This->allTables = allocDefVectorTable();
        This->allOrders = allocDefVectorOrder();
        This->allFunctions = allocDefVectorFunction();
+       This->satEncoder = allocSATEncoder();
        return This;
 }
 
@@ -68,6 +70,7 @@ void deleteSolver(CSolver *This) {
                deleteFunction(getVectorFunction(This->allFunctions, i));
        }
        deleteVectorFunction(This->allFunctions);
+       deleteSATEncoder(This->satEncoder);
        ourfree(This);
 }
 
@@ -173,7 +176,7 @@ Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t
 
 void startEncoding(CSolver* This){
        naiveEncodingDecision(This);
-       SATEncoder* satEncoder = allocSATEncoder();
+       SATEncoder* satEncoder = This->satEncoder;
        encodeAllSATEncoder(This, satEncoder);
        int result= solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
@@ -181,7 +184,25 @@ void startEncoding(CSolver* This){
                model_print("%d, ", satEncoder->cnf->solver->solution[i]);
        }
        model_print("\n");
-       //For now, let's just delete it, and in future for doing queries 
-       //we may need it.
-       deleteSATEncoder(satEncoder);
+}
+
+uint64_t getElementValue(CSolver* This, Element* element){
+       switch(GETELEMENTTYPE(element)){
+               case ELEMSET:
+                       return getElementValueSATTranslator(This, element);
+                       break;
+               default:
+                       ASSERT(0);
+       }
+       return -1;
+}
+
+bool getBooleanValue( CSolver* This , Boolean* boolean){
+       switch(GETBOOLEANTYPE(boolean)){
+               case BOOLEANVAR:
+                       return getBooleanVariableValueSATTranslator(This, boolean);
+               default:
+                       ASSERT(0);
+       }
+       return -1;
 }

diff --git a/src/csolver.h b/src/csolver.h
index 827609c94abe3094f0d70c93add5e89949f44ec7..9628f11b2e8d17c059acbf239d006c12c3b2f500 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -5,6 +5,7 @@
 #include "structs.h"
 
 struct CSolver {
+       SATEncoder* satEncoder;
        /** This is a vector of constraints that must be satisfied. */
        VectorBoolean * constraints;
 
@@ -114,4 +115,11 @@ Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t sec
 
 /** When everything is done, the client calls this function and then csolver starts to encode*/
 void startEncoding(CSolver*);
+
+/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
+uint64_t getElementValue(CSolver*, Element* element);
+
+/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
+bool getBooleanValue( CSolver* , Boolean* boolean);
+
 #endif