diff options
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 24 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 12 |
2 files changed, 18 insertions, 18 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))); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index dc06753ab..549c0b679 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -44,8 +44,8 @@ public: static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(Minisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Minisat::lbool res); static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause); static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause); @@ -56,14 +56,14 @@ public: SatVariable newVar(bool theoryAtom = false); - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); + SatValue solve(); + SatValue solve(long unsigned int&); void interrupt(); - SatLiteralValue value(SatLiteral l); + SatValue value(SatLiteral l); - SatLiteralValue modelValue(SatLiteral l); + SatValue modelValue(SatLiteral l); bool properExplanation(SatLiteral lit, SatLiteral expl) const; |