From 0c6a9f7ee5ad540cf01e4fb4a1d3506505948ac2 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 11 Jul 2017 18:51:58 -0700
Subject: [PATCH] Adding SAT translator

---
 src/Backend/sattranslator.c | 41 +++++++++++++++++++++++++++++++++++++
 src/Backend/sattranslator.h | 17 +++++++++++++++
 src/csolver.c               | 29 ++++++++++++++++++++++----
 src/csolver.h               |  8 ++++++++
 4 files changed, 91 insertions(+), 4 deletions(-)
 create mode 100644 src/Backend/sattranslator.c
 create mode 100644 src/Backend/sattranslator.h

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
new file mode 100644
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
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 40490d5..c12b7ce 100644
--- 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 827609c..9628f11 100644
--- 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
-- 
2.34.1