diff options
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ede18c585..1ec81a4f6 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -57,16 +57,16 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { Minisat::sign(lit)); } -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; +SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + else return SAT_VALUE_FALSE; } -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { - if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown; +SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { + if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; + if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (Minisat::lbool((uint8_t)1))); - return SatValFalse; + return SAT_VALUE_FALSE; } @@ -121,7 +121,7 @@ SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { } -SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { +SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -130,14 +130,14 @@ SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { } Minisat::vec<Minisat::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") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; return result; } -SatLiteralValue DPLLMinisatSatSolver::solve() { +SatValue DPLLMinisatSatSolver::solve() { d_minisat->budgetOff(); return toSatLiteralValue(d_minisat->solve()); } @@ -147,11 +147,11 @@ void DPLLMinisatSatSolver::interrupt() { d_minisat->interrupt(); } -SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) { +SatValue DPLLMinisatSatSolver::value(SatLiteral l) { return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } -SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ +SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } |