Integrating with sat_solver ...
authorHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 19:12:40 +0000 (12:12 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Mon, 10 Jul 2017 19:12:40 +0000 (12:12 -0700)
.gitignore
src/Backend/constraint.h
src/Backend/satencoder.c
src/Backend/satencoder.h
src/Test/buildconstraints.c
src/csolver.c

index c6f1f57..2d1b9f1 100644 (file)
@@ -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
index e1b21d3..964c697 100644 (file)
@@ -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;}
index e78cb3f..4a72f0a 100644 (file)
 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?
        }
 }
 
index 36cbc77..0ada52b 100644 (file)
@@ -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
index 81f01b3..c91fd57 100644 (file)
@@ -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);
 }
index d63c266..985122f 100644 (file)
@@ -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);