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 0dad2989374bace0abf19b936af3cc740b1b07f9..7e20f56c34b446e87422662f386ed6e12cc8603f 100644 (file)
--- 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<Node>& 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 d4aedad8a291e5ce863c54f0afacc1d20259d6bc..8f91d921be4f145f8b9b05a96e5cf795b7e3c250 100644 (file)
--- 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 5cf7122f31eddfb6f1f0b08782d5b2063fe3d605..0dfa0141f8c097537f48e1a7c7104c3eeed302b8 100644 (file)
--- 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 0cbd96914b21e371bd54a225f998b80e5205149c..52a4ad70b7af53cc524d33cb7c49b402baef6bea 100644 (file)
--- 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 4a8d0406b22ea45c9f19ca3636f4aa9cb00c32bc..2b6719b27fcf62f5a253b842af535437bd365e49 100644 (file)
--- 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 ce6c810119fb5bf8c34f0edf76c73adce0b58b1b..e6a1ee514427a730172d5e094bd9200a455c85f2 100644 (file)
--- 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 <unordered_set>
+
 #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;
   /**