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);