diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-12-14 13:14:59 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-14 10:14:59 -0600 |
| commit | c51920039f10864f813ae1a4b4e765264a322256 (patch) | |
| tree | 5ff31e640bc08882252a39a0255614359f03c62a /src/decision | |
| parent | dddddbfa12aaeb433074382fb9e2b4c9c92c8a66 (diff) | |
[proof-new] Updating interfaces between prop engine and minisat (#5664)
This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".
Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.
Diffstat (limited to 'src/decision')
| -rw-r--r-- | src/decision/decision_engine.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index afa16397d..15dbf0d79 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -46,7 +46,7 @@ class DecisionEngine { // PropEngine* d_propEngine; CnfStream* d_cnfStream; - DPLLSatSolverInterface* d_satSolver; + CDCLTSatSolverInterface* d_satSolver; context::Context* d_satContext; context::UserContext* d_userContext; @@ -75,7 +75,8 @@ class DecisionEngine { Trace("decision") << "Destroying decision engine" << std::endl; } - void setSatSolver(DPLLSatSolverInterface* ss) { + void setSatSolver(CDCLTSatSolverInterface* ss) + { // setPropEngine should not be called more than once Assert(d_satSolver == NULL); Assert(ss != NULL); |