diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-02 16:20:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-02 16:20:45 -0700 |
commit | 5001fa069ab42134333244b3f27c852724cea3e2 (patch) | |
tree | c03b1730016a03094064b01311d5a529d9e00641 /src | |
parent | 902262c421e52405204b3a95310c8414cc51a5c5 (diff) |
Update CaDiCaL to version 1.0.3. (#3137)
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
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(); } |