Integrating with sat_solver ...

diff --git a/.gitignore b/.gitignore
index c6f1f574662b4884c0eb0a4685521ddf784b8e0a..2d1b9f1b8d7cd96e8299ce2f07102a6b4914e384 100644 (file)
--- 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 e1b21d36f69f4ea5ec45ebb646a39b3024e4b16a..964c697be1649cb5a174e678e99248632a4c3d07 100644 (file)
--- 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 e78cb3f634764c3d65fd68b971b313f087745c61..4a72f0abd54d8cbac585d8d4e5d0310e740bc2c4 100644 (file)
--- 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 36cbc7727a95df9241e114217dfd9df01010ab6f..0ada52b1bc239d1817cc09d89c04a7c305fe0849 100644 (file)
--- 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 81f01b3988c38deac8bbd87ed16560bfeb2c5f70..c91fd571294e276c65072854989be2eb38fea878 100644 (file)
--- 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 d63c266c804aa2bf587e76db54bda52d939cafcb..985122fc96400948ed543a2306abefba924c289b 100644 (file)
--- 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);