From: Andrew Reynolds Date: Fri, 3 Sep 2021 16:33:27 +0000 (-0500) Subject: Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133) X-Git-Tag: cvc5-1.0.0~1277 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39dd4cf7678da7bbce2a0aaf4d9b44d3f885ea49;p=cvc5.git Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133) --- diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index b773d8d57..b66daefd3 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -32,13 +32,11 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent) - : d_env(env), d_parent(parent) -{ -} +AbductionSolver::AbductionSolver(Env& env) : EnvObj(env) {} AbductionSolver::~AbductionSolver() {} -bool AbductionSolver::getAbduct(const Node& goal, +bool AbductionSolver::getAbduct(const std::vector& axioms, + const Node& goal, const TypeNode& grammarType, Node& abd) { @@ -48,7 +46,6 @@ bool AbductionSolver::getAbduct(const Node& goal, throw ModalException(msg); } Trace("sygus-abduct") << "SmtEngine::getAbduct: goal " << goal << std::endl; - std::vector axioms = d_parent->getExpandedAssertions(); std::vector asserts(axioms.begin(), axioms.end()); // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(goal); @@ -74,16 +71,19 @@ bool AbductionSolver::getAbduct(const Node& goal, d_subsolver->setLogic(l); // assert the abduction query d_subsolver->assertFormula(aconj); - return getAbductInternal(abd); + return getAbductInternal(axioms, abd); } -bool AbductionSolver::getAbduct(const Node& goal, Node& abd) +bool AbductionSolver::getAbduct(const std::vector& axioms, + const Node& goal, + Node& abd) { TypeNode grammarType; - return getAbduct(goal, grammarType, abd); + return getAbduct(axioms, goal, grammarType, abd); } -bool AbductionSolver::getAbductInternal(Node& abd) +bool AbductionSolver::getAbductInternal(const std::vector& axioms, + Node& abd) { // should have initialized the subsolver by now Assert(d_subsolver != nullptr); @@ -128,7 +128,7 @@ bool AbductionSolver::getAbductInternal(Node& abd) // if check abducts option is set, we check the correctness if (options::checkAbducts()) { - checkAbduct(abd); + checkAbduct(axioms, abd); } return true; } @@ -139,13 +139,13 @@ bool AbductionSolver::getAbductInternal(Node& abd) return false; } -void AbductionSolver::checkAbduct(Node a) +void AbductionSolver::checkAbduct(const std::vector& axioms, Node a) { Assert(a.getType().isBoolean()); Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions" << std::endl; - std::vector asserts = d_parent->getExpandedAssertions(); + std::vector asserts(axioms.begin(), axioms.end()); asserts.push_back(a); // two checks: first, consistent with assertions, second, implies negated goal diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h index b408fe060..3ea2755ae 100644 --- a/src/smt/abduction_solver.h +++ b/src/smt/abduction_solver.h @@ -20,10 +20,10 @@ #include "expr/node.h" #include "expr/type_node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; class SmtEngine; namespace smt { @@ -35,10 +35,10 @@ namespace smt { * a subsolver SmtEngine for a sygus conjecture that captures the abduction * query, and implements supporting utility methods such as checkAbduct. */ -class AbductionSolver +class AbductionSolver : protected EnvObj { public: - AbductionSolver(Env& env, SmtEngine* parent); + AbductionSolver(Env& env); ~AbductionSolver(); /** * This method asks this SMT engine to find an abduct with respect to the @@ -46,23 +46,27 @@ class AbductionSolver * If this method returns true, then abd is set to a formula C such that * A ^ C is satisfiable, and A ^ ~B ^ C is unsatisfiable. * - * @param goal The goal of the abduction problem. + * @param axioms The expanded assertions A of the parent SMT engine + * @param goal The goal B of the abduction problem. * @param grammarType A sygus datatype type that encodes the syntax * restrictions on the shape of possible solutions. - * @param abd This argument is updated to contain the solution to the + * @param abd This argument is updated to contain the solution C to the * abduction problem. Notice that this is a formula whose free symbols * are contained in goal + the parent's current assertion stack. * * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getAbduct(const Node& goal, const TypeNode& grammarType, Node& abd); + bool getAbduct(const std::vector& axioms, + const Node& goal, + const TypeNode& grammarType, + Node& abd); /** * Same as above, but without user-provided grammar restrictions. A default * grammar is chosen internally using the sygus grammar constructor utility. */ - bool getAbduct(const Node& goal, Node& abd); + bool getAbduct(const std::vector& axioms, const Node& goal, Node& abd); /** * Check that a solution to an abduction conjecture is indeed a solution. @@ -71,8 +75,11 @@ class AbductionSolver * solution to the abduction problem (a) is SAT, and the assertions conjoined * with the abduct and the goal is UNSAT. If these criteria are not met, an * internal error is thrown. + * + * @param axioms The expanded assertions of the parent SMT engine + * @param a The abduct to check. */ - void checkAbduct(Node a); + void checkAbduct(const std::vector& axioms, Node a); private: /** @@ -84,11 +91,7 @@ class AbductionSolver * This method assumes d_subsolver has been initialized to do abduction * problems. */ - bool getAbductInternal(Node& abd); - /** Reference to the env */ - Env& d_env; - /** The parent SMT engine */ - SmtEngine* d_parent; + bool getAbductInternal(const std::vector& axioms, Node& abd); /** The SMT engine subsolver * * This is a separate copy of the SMT engine which is used for making diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index ab7002205..3e227fa31 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -32,14 +32,12 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent) - : d_env(env), d_parent(parent) -{ -} +InterpolationSolver::InterpolationSolver(Env& env) : EnvObj(env) {} InterpolationSolver::~InterpolationSolver() {} -bool InterpolationSolver::getInterpol(const Node& conj, +bool InterpolationSolver::getInterpol(const std::vector& axioms, + const Node& conj, const TypeNode& grammarType, Node& interpol) { @@ -51,7 +49,6 @@ bool InterpolationSolver::getInterpol(const Node& conj, } Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj << std::endl; - std::vector axioms = d_parent->getExpandedAssertions(); // must expand definitions Node conjn = d_env.getTopLevelSubstitutions().apply(conj); std::string name("A"); @@ -69,10 +66,12 @@ bool InterpolationSolver::getInterpol(const Node& conj, return false; } -bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol) +bool InterpolationSolver::getInterpol(const std::vector& axioms, + const Node& conj, + Node& interpol) { TypeNode grammarType; - return getInterpol(conj, grammarType, interpol); + return getInterpol(axioms, conj, grammarType, interpol); } void InterpolationSolver::checkInterpol(Node interpol, diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 19bb54c61..03c899ead 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -20,12 +20,9 @@ #include "expr/node.h" #include "expr/type_node.h" +#include "smt/env_obj.h" namespace cvc5 { - -class Env; -class SmtEngine; - namespace smt { /** @@ -35,28 +32,30 @@ namespace smt { * a subsolver SmtEngine for a sygus conjecture that captures the interpolation * query, and implements supporting utility methods such as checkInterpol. */ -class InterpolationSolver +class InterpolationSolver : protected EnvObj { public: - InterpolationSolver(Env& env, SmtEngine* parent); + InterpolationSolver(Env& env); ~InterpolationSolver(); /** - * This method asks this SMT engine to find an interpolant with respect to + * This method asks this solver to find an interpolant with respect to * the current assertion stack (call it A) and the conjecture (call it B). If * this method returns true, then interpolant is set to a formula I such that * A ^ ~I and I ^ ~B are both unsatisfiable. * - * @param conj The conjecture of the interpolation problem. + * @param axioms The expanded assertions A of the parent SMT engine + * @param conj The conjecture B of the interpolation problem. * @param grammarType A sygus datatype type that encodes the syntax * restrictions on the shape of possible solutions. - * @param interpol This argument is updated to contain the solution to the + * @param interpol This argument is updated to contain the solution I to the * interpolation problem. * * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getInterpol(const Node& conj, + bool getInterpol(const std::vector& axioms, + const Node& conj, const TypeNode& grammarType, Node& interpol); @@ -64,7 +63,9 @@ class InterpolationSolver * Same as above, but without user-provided grammar restrictions. A default * grammar is chosen internally using the sygus grammar constructor utility. */ - bool getInterpol(const Node& conj, Node& interpol); + bool getInterpol(const std::vector& axioms, + const Node& conj, + Node& interpol); /** * Check that a solution to an interpolation problem is indeed a solution. @@ -76,12 +77,6 @@ class InterpolationSolver void checkInterpol(Node interpol, const std::vector& easserts, const Node& conj); - - private: - /** Reference to the env */ - Env& d_env; - /** The parent SMT engine */ - SmtEngine* d_parent; }; } // namespace smt diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 72268aa03..582ca0c2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -255,12 +255,12 @@ void SmtEngine::finishInit() // subsolvers if (d_env->getOptions().smt.produceAbducts) { - d_abductSolver.reset(new AbductionSolver(*d_env.get(), this)); + d_abductSolver.reset(new AbductionSolver(*d_env.get())); } if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { - d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this)); + d_interpolSolver.reset(new InterpolationSolver(*d_env.get())); } d_pp->finishInit(); @@ -1754,7 +1754,9 @@ bool SmtEngine::getInterpol(const Node& conj, { SmtScope smts(this); finishInit(); - bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); + std::vector axioms = getExpandedAssertions(); + bool success = + d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); @@ -1773,7 +1775,8 @@ bool SmtEngine::getAbduct(const Node& conj, { SmtScope smts(this); finishInit(); - bool success = d_abductSolver->getAbduct(conj, grammarType, abd); + std::vector axioms = getExpandedAssertions(); + bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); // notify the state of whether the get-abduct call was successfuly, which // impacts the SMT mode. d_state->notifyGetAbduct(success);