diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-16 12:45:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 12:45:01 -0500 |
| commit | 2c2f05c96e021006275a2bc70b9ede70b280616d (patch) | |
| tree | db702d7b8fbd14dd8003b1f03c02b77c89d2fced /src/smt/smt_solver.cpp | |
| parent | 0534ea1bbee9a3a7049580449ab25025a4f92a9a (diff) | |
Dump commands in internal code using command printing functions. (#5040)
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
Diffstat (limited to 'src/smt/smt_solver.cpp')
| -rw-r--r-- | src/smt/smt_solver.cpp | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c64689be6..922831106 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -51,7 +51,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_smt.getUserContext(), d_rm, d_pp.getTermFormulaRemover(), - logicInfo)); + logicInfo, + d_smt.getOutputManager())); // Add the theories for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; @@ -65,8 +66,11 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -82,8 +86,11 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine( - d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm)); + d_propEngine.reset(new PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager())); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not |