From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 10 Jul 2017 19:12:40 +0000 (-0700)
Subject: Integrating with sat_solver ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c0e5beecb1d6ca75881cb4972642305ce607699f;p=satune.git

Integrating with sat_solver ...
---

diff --git a/.gitignore b/.gitignore
index c6f1f57..2d1b9f1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,9 +1,11 @@
 #Ignoring netbeans configs
 nbproject/
+sat_solver
+setup.sh
 
 #Ignoring binary files
 src/bin/
 src/lib_cons_comp.so
 /src/mymemory.cc
 .*
-*.dSYM
\ No newline at end of file
+*.dSYM
diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index e1b21d3..964c697 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -34,7 +34,7 @@ void deleteConstraint(Constraint *);
 void printConstraint(Constraint * c);
 void dumpConstraint(Constraint * c, IncrementalSolver *solver);
 static inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
-VectorConstraint * simplify(Constraint * c);
+VectorConstraint * simplifyConstraint(Constraint * This);
 static inline CType getType(Constraint * c) {return c->type;}
 static inline bool isFalse(Constraint * c) {return c->type==FALSE;}
 static inline bool isTrue(Constraint * c) {return c->type==TRUE;}
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index e78cb3f..4a72f0a 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -16,10 +16,12 @@
 SATEncoder * allocSATEncoder() {
 	SATEncoder *This=ourmalloc(sizeof (SATEncoder));
 	This->varcount=1;
+	This->satSolver = allocIncrementalSolver();
 	return This;
 }
 
 void deleteSATEncoder(SATEncoder *This) {
+	deleteIncrementalSolver(This->satSolver);
 	ourfree(This);
 }
 
@@ -27,6 +29,7 @@ Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64
 	generateElementEncodingVariables(encoder, getElementEncoding(This));
 	switch(getElementEncoding(This)->type){
 		case ONEHOT:
+			//FIXME
 			ASSERT(0);
 			break;
 		case UNARY:
@@ -60,14 +63,30 @@ Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value)
 	return NULL;
 }
 
+void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver) {
+	VectorConstraint* simplified = simplifyConstraint(c);
+	uint size = getSizeVectorConstraint(simplified);
+	for(uint i=0; i<size; i++) {
+		Constraint *simp=getVectorConstraint(simplified, i);
+		if (simp->type==TRUE)
+			continue;
+		ASSERT(simp->type!=FALSE);
+		dumpConstraint(simp, satSolver);
+	}
+	deleteVectorConstraint(simplified);
+}
+
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 	VectorBoolean *constraints=csolver->constraints;
 	uint size=getSizeVectorBoolean(constraints);
 	for(uint i=0;i<size;i++) {
 		Boolean *constraint=getVectorBoolean(constraints, i);
 		Constraint* c= encodeConstraintSATEncoder(This, constraint);
+		addConstraintToSATSolver(c, This->satSolver);
 		printConstraint(c);
 		model_print("\n\n");
+		//FIXME: When do we want to delete constraints? Should we keep an array of them
+		// and delete them later, or it would be better to just delete them right away?
 	}
 }
 
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 36cbc77..0ada52b 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -3,9 +3,11 @@
 
 #include "classlist.h"
 #include "structs.h"
+#include "inc_solver.h"
 
 struct SATEncoder {
 	uint varcount;
+	IncrementalSolver* satSolver;
 };
 
 SATEncoder * allocSATEncoder();
@@ -35,4 +37,5 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
+void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver);
 #endif
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 81f01b3..c91fd57 100644
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -38,6 +38,6 @@ int main(int numargs, char ** argv) {
 	Element* inputs2 [] = {e4, e3};
 	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
 	addBoolean(solver, pred);
-	startEncoding(solver);
+//	startEncoding(solver);
 	deleteSolver(solver);
 }
diff --git a/src/csolver.c b/src/csolver.c
index d63c266..985122f 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,8 +174,13 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
 void startEncoding(CSolver* solver){
 	naiveEncodingDecision(solver);
 	SATEncoder* satEncoder = allocSATEncoder();
-//	initializeConstraintVars(solver, satEncoder);
+	createSolver(satEncoder->satSolver);
 	encodeAllSATEncoder(solver, satEncoder);
+	finishedClauses(satEncoder->satSolver);
+	solve(satEncoder->satSolver);
+	int result= getSolution(satEncoder->satSolver);
+	model_print("sat_solver's result:%d\n", result);
+	killSolver(satEncoder->satSolver);
 	//For now, let's just delete it, and in future for doing queries 
 	//we may need it.
 	deleteSATEncoder(satEncoder);