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/prop | |
| 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/prop')
| -rw-r--r-- | src/prop/cadical.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
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(); } |