diff options
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) |