diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/options_handler.cpp | 11 | ||||
-rw-r--r-- | src/prop/cadical.cpp | 10 |
2 files changed, 4 insertions, 17 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 15436646f..b0a1cd1ad 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1174,17 +1174,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, } else if (optarg == "cadical") { -#ifndef CVC4_INCREMENTAL_CADICAL - if (options::incrementalSolving() - && options::incrementalSolving.wasSetByUser()) - { - throw OptionException(std::string( - "CaDiCaL version used does not support incremental mode. \n\ - Update CaDiCal or Try --bv-sat-solver=cryptominisat or " - "--bv-sat-solver=minisat")); - } -#endif - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && options::bitblastMode.wasSetByUser()) { diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index b4851f945..479ec2414 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -37,10 +37,12 @@ SatValue toSatValue(int result) return SAT_VALUE_UNKNOWN; } +/* Note: CaDiCaL returns lit/-lit for true/false. Older versions returned 1/-1. + */ SatValue toSatValueLit(int value) { - if (value == 1) return SAT_VALUE_TRUE; - Assert(value == -1); + if (value > 0) return SAT_VALUE_TRUE; + Assert(value < 0); return SAT_VALUE_FALSE; } @@ -119,7 +121,6 @@ SatValue CadicalSolver::solve(long unsigned int&) SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions) { -#ifdef CVC4_INCREMENTAL_CADICAL TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); for (const SatLiteral& lit : assumptions) { @@ -129,9 +130,6 @@ SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions) d_okay = (res == SAT_VALUE_TRUE); ++d_statistics.d_numSatCalls; return res; -#else - Unimplemented("CaDiCaL version used does not support incremental solving"); -#endif } void CadicalSolver::interrupt() { d_solver->terminate(); } |