diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-26 11:55:59 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-26 16:55:59 +0000 |
commit | 21fa888738ea77e4436ef164c184e61683a55fb5 (patch) | |
tree | af76cfe9dbbb082ee8e2ed73afa974daf2fb0f07 /src/smt/abduction_solver.cpp | |
parent | 6cf3a69a9afd68922d67941c6fd2b877df45ecb9 (diff) |
Eliminate currentSmtEngine for subsolver calls (#7068)
This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.
Diffstat (limited to 'src/smt/abduction_solver.cpp')
-rw-r--r-- | src/smt/abduction_solver.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index ff1337fe1..b773d8d57 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -32,7 +32,10 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {} +AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent) + : d_env(env), d_parent(parent) +{ +} AbductionSolver::~AbductionSolver() {} bool AbductionSolver::getAbduct(const Node& goal, @@ -48,7 +51,7 @@ bool AbductionSolver::getAbduct(const Node& goal, std::vector<Node> axioms = d_parent->getExpandedAssertions(); std::vector<Node> asserts(axioms.begin(), axioms.end()); // must expand definitions - Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal); + Node conjn = d_env.getTopLevelSubstitutions().apply(goal); // now negate conjn = conjn.negate(); d_abdConj = conjn; @@ -63,7 +66,7 @@ bool AbductionSolver::getAbduct(const Node& goal, Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj << ", solving for " << d_sssf << std::endl; // we generate a new smt engine to do the abduction query - initializeSubsolver(d_subsolver); + initializeSubsolver(d_subsolver, d_env); // get the logic LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus @@ -153,7 +156,7 @@ void AbductionSolver::checkAbduct(Node a) << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution std::unique_ptr<SmtEngine> abdChecker; - initializeSubsolver(abdChecker); + initializeSubsolver(abdChecker, d_env); Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": asserting formulas" << std::endl; for (const Node& e : asserts) |