diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 14:22:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-26 14:22:38 +0000 |
commit | 1ed3b1803bd0a25c56a62d290cd5dcb64c5085ce (patch) | |
tree | f65a0b2ad744a5f2b6408c34319aad10c7d2f406 /src/prop/bvminisat | |
parent | 9918f0e86a38f5fc8671ec6115eaac9b2c3b31d8 (diff) |
More cleaning up.
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 32 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 14 |
2 files changed, 23 insertions, 23 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 3d2d4c9ea..c4c21e126 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -54,11 +54,11 @@ void MinisatSatSolver::interrupt(){ d_minisat->interrupt(); } -SatLiteralValue MinisatSatSolver::solve(){ +SatValue MinisatSatSolver::solve(){ return toSatLiteralValue(d_minisat->solve()); } -SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ +SatValue MinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -67,14 +67,14 @@ SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ } BVMinisat::vec<BVMinisat::Lit> empty; unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); d_minisat->clearInterrupt(); resource = d_minisat->conflicts - conflictsBefore; Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl; return result; } -SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){ +SatValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){ Debug("sat::minisat") << "Solve with assumptions "; context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); BVMinisat::vec<BVMinisat::Lit> assump; @@ -85,7 +85,7 @@ SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assu } Debug("sat::minisat") <<"\n"; - SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); + SatValue result = toSatLiteralValue(d_minisat->solve(assump)); return result; } @@ -97,14 +97,14 @@ void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) { } } -SatLiteralValue MinisatSatSolver::value(SatLiteral l){ +SatValue MinisatSatSolver::value(SatLiteral l){ Unimplemented(); - return SatValUnknown; + return SAT_VALUE_UNKNOWN; } -SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ +SatValue MinisatSatSolver::modelValue(SatLiteral l){ Unimplemented(); - return SatValUnknown; + return SAT_VALUE_UNKNOWN; } void MinisatSatSolver::unregisterVar(SatLiteral lit) { @@ -150,16 +150,16 @@ SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { BVMinisat::sign(lit)); } -SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; +SatValue MinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + else return SAT_VALUE_FALSE; } -SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { - if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; +SatValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { + if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; + if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (BVMinisat::lbool((uint8_t)1))); - return SatValFalse; + return SAT_VALUE_FALSE; } void MinisatSatSolver::toMinisatClause(SatClause& clause, diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index ed164904e..043aa5d24 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -38,13 +38,13 @@ public: void interrupt(); - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); - SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions); + SatValue solve(); + SatValue solve(long unsigned int&); + SatValue solve(const context::CDList<SatLiteral> & assumptions); void getUnsatCore(SatClause& unsatCore); - SatLiteralValue value(SatLiteral l); - SatLiteralValue modelValue(SatLiteral l); + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); @@ -56,8 +56,8 @@ public: static SatVariable toSatVariable(BVMinisat::Var var); static BVMinisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(BVMinisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(BVMinisat::lbool res); static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); |