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/prop/prop_engine.cpp | |
| 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/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e5efcbf8f..fee73babb 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -70,7 +70,8 @@ PropEngine::PropEngine(TheoryEngine* te, Context* satContext, UserContext* userContext, ResourceManager* rm, - OutputManager& outMgr) + OutputManager& outMgr, + ProofNodeManager* pnm) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), @@ -79,6 +80,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar(NULL), d_cnfStream(NULL), d_pfCnfStream(nullptr), + d_ppm(nullptr), d_interrupted(false), d_resourceManager(rm), d_outMgr(outMgr) @@ -89,7 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies - d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); + d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( @@ -97,7 +99,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy( this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); - d_satSolver->initialize(d_context, d_theoryProxy); + d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); |