diff options
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 4f2a16670..6b02153c7 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -69,6 +69,20 @@ SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { return SAT_VALUE_FALSE; } +Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0); + if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2); + Assert(val == SAT_VALUE_FALSE); + return Minisat::lbool((uint8_t)1); +} + +/*bool MinisatSatSolver::tobool(SatValue val) +{ + if(val == SAT_VALUE_TRUE) return true; + Assert(val == SAT_VALUE_FALSE); + return false; + }*/ void MinisatSatSolver::toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause) { @@ -92,10 +106,15 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; + if( Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ) { + Notice() << "minisat: Incremental solving is disabled" + << " unless using internal decision strategy." << std::endl; + } + // Create the solver d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, Options::current()->incrementalSolving || - Options::current()->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION ); + Options::current()->decisionMode != Options::DECISION_STRATEGY_INTERNAL ); // Setup the verbosity d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; |