From: Aina Niemetz Date: Fri, 3 Sep 2021 22:36:44 +0000 (-0700) Subject: sygus: Make more classes derive from EnvObj. (#7140) X-Git-Tag: cvc5-1.0.0~1270 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=54212c1402e43d3a414d20f3e418f2a0fec10a8d;p=cvc5.git sygus: Make more classes derive from EnvObj. (#7140) --- diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 0dad29893..7e20f56c3 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -26,14 +26,13 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" -#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" namespace cvc5 { namespace theory { namespace quantifiers { -SygusInterpol::SygusInterpol(Env& env) : d_env(env) {} +SygusInterpol::SygusInterpol(Env& env) : EnvObj(env) {} void SygusInterpol::collectSymbols(const std::vector& axioms, const Node& conj) @@ -255,7 +254,7 @@ void SygusInterpol::mkSygusConjecture(Node itp, constraint = constraint.substitute( d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end()); Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl; - constraint = Rewriter::rewrite(constraint); + constraint = rewrite(constraint); d_sygusConj = constraint; Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index d4aedad8a..8f91d921b 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/type_node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -59,7 +60,7 @@ namespace quantifiers { * of the SMT engine can be further queried for information regarding further * solutions. */ -class SygusInterpol +class SygusInterpol : protected EnvObj { public: SygusInterpol(Env& env); @@ -174,8 +175,6 @@ class SygusInterpol * @param itp the interpolation predicate. */ bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp); - /** Reference to the env */ - Env& d_env; /** * symbols from axioms and conjecture. */ diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index 5cf7122f3..0dfa0141f 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -18,7 +18,6 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "theory/quantifiers/single_inv_partition.h" -#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace cvc5::kind; @@ -27,7 +26,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusQePreproc::SygusQePreproc(Env& env) : d_env(env) {} +SygusQePreproc::SygusQePreproc(Env& env) : EnvObj(env) {} Node SygusQePreproc::preprocess(Node q) { @@ -134,7 +133,7 @@ Node SygusQePreproc::preprocess(Node q) qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]); Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes << std::endl; - qeRes = Rewriter::rewrite(qeRes); + qeRes = rewrite(qeRes); Node nq = qeRes; // must assert it is equivalent to the original Node lem = q.eqNode(nq); diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 0cbd96914..52a4ad70b 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -17,6 +17,7 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -35,7 +36,7 @@ namespace quantifiers { * exists f. forall x. Q[ f(x), x ] * For more details, see Example 6 of Reynolds et al. SYNT 2017. */ -class SygusQePreproc +class SygusQePreproc : protected EnvObj { public: SygusQePreproc(Env& env); @@ -45,10 +46,6 @@ class SygusQePreproc * by the quantifier elimination technique outlined above. */ Node preprocess(Node q); - - private: - /** Reference to the env */ - Env& d_env; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 4a8d0406b..2b6719b27 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -35,7 +35,7 @@ namespace theory { namespace quantifiers { SygusRepairConst::SygusRepairConst(Env& env, TermDbSygus* tds) - : d_env(env), d_tds(tds), d_allow_constant_grammar(false) + : EnvObj(env), d_tds(tds), d_allow_constant_grammar(false) { } @@ -189,7 +189,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, // check whether it is not in the current logic, e.g. non-linear arithmetic. // if so, undo replacements until it is in the current logic. - const LogicInfo& logic = d_env.getLogicInfo(); + const LogicInfo& logic = getLogicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { fo_body = fitToLogic(sygusBody, diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index ce6c81011..e6a1ee514 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -19,7 +19,9 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H #include + #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -46,7 +48,7 @@ class TermDbSygus; * within repairSolution(...) below, which if satisfiable gives us the * valuation for c'. */ -class SygusRepairConst +class SygusRepairConst : protected EnvObj { public: SygusRepairConst(Env& env, TermDbSygus* tds); @@ -106,8 +108,6 @@ class SygusRepairConst static bool mustRepair(Node n); private: - /** Reference to the env */ - Env& d_env; /** pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; /**