sygus: Make CeSingleInv derive from EnvObj. (#7136)

This further reorders the header according to the code style guidelines.

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 99716806f4bafb101a9118eb20dd81c3c440a283..d2c616238c2655cf7c7423783c2c5806da1631bc 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -28,7 +28,6 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace cvc5::kind;
@@ -38,10 +37,10 @@ namespace theory {
 namespace quantifiers {
 
 CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s)
-    : d_env(env),
+    : EnvObj(env),
+      d_isSolved(false),
       d_sip(new SingleInvocationPartition),
       d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)),
-      d_isSolved(false),
       d_single_invocation(false),
       d_treg(tr)
 {
@@ -277,7 +276,7 @@ bool CegSingleInv::solve()
       Assert(inst.size() == vars.size());
       Node ilem =
           body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
-      ilem = Rewriter::rewrite(ilem);
+      ilem = rewrite(ilem);
       d_instConds.push_back(ilem);
       Trace("sygus-si") << "  Instantiation Lemma: " << ilem << std::endl;
     }
@@ -512,7 +511,7 @@ bool CegSingleInv::solveTrivial(Node q)
       // remake with eliminated nodes
       body = body.substitute(
           varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
-      body = Rewriter::rewrite(body);
+      body = rewrite(body);
       // apply to subs
       // this ensures we behave correctly if we solve x before y in
       // x = y+1 ^ y = 2.
@@ -520,7 +519,7 @@ bool CegSingleInv::solveTrivial(Node q)
       {
         subs[i] = subs[i].substitute(
             varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
-        subs[i] = Rewriter::rewrite(subs[i]);
+        subs[i] = rewrite(subs[i]);
       }
       vars.insert(vars.end(), varsTmp.begin(), varsTmp.end());
       subs.insert(subs.end(), subsTmp.begin(), subsTmp.end());

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index f7d6e5bb99bc0008f05755c24ed9a2cba7bae836..a0fac61d3002abde485d3c7da9619e2dc39f0ac2 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -20,6 +20,7 @@
 
 #include "context/cdlist.h"
 #include "expr/subs.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/single_inv_partition.h"
@@ -40,63 +41,13 @@ class SygusReconstruct;
 // (2) inferring whether the conjecture corresponds to a deterministic transistion system (by utility d_ti).
 // For these techniques, we may generate a template (d_templ) which specifies a restricted
 // solution space. We may in turn embed this template as a SyGuS grammar.
-class CegSingleInv
+class CegSingleInv : protected EnvObj
 {
- private:
-  //presolve
-  void collectPresolveEqTerms( Node n,
-                               std::map< Node, std::vector< Node > >& teq );
-  void getPresolveEqConjuncts( std::vector< Node >& vars,
-                               std::vector< Node >& terms,
-                               std::map< Node, std::vector< Node > >& teq,
-                               Node n, std::vector< Node >& conj );
- private:
-  /** Reference to the env */
-  Env& d_env;
-  // single invocation inference utility
-  SingleInvocationPartition* d_sip;
-  /** solution reconstruction */
-  std::unique_ptr<SygusReconstruct> d_srcons;
-
-  // list of skolems for each argument of programs
-  std::vector<Node> d_single_inv_arg_sk;
-  // program to solution index
-  std::map<Node, unsigned> d_prog_to_sol_index;
-  // original conjecture
-  Node d_orig_conjecture;
-
- public:
-  //---------------------------------representation of the solution
-  /**
-   * The list of instantiations that suffice to show the first-order equivalent
-   * of the negated synthesis conjecture is unsatisfiable.
-   */
-  std::vector<std::vector<Node> > d_inst;
-  /**
-   * The list of instantiation lemmas, corresponding to instantiations of the
-   * first order conjecture for the term vectors above.
-   */
-  std::vector<Node> d_instConds;
-  /** The solutions, without reconstruction to syntax */
-  std::vector<Node> d_solutions;
-  /** The solutions, after reconstruction to syntax */
-  std::vector<Node> d_rcSolutions;
-  /** is solved */
-  bool d_isSolved;
-  //---------------------------------end representation of the solution
-
- private:
-  Node d_simp_quant;
-  // are we single invocation?
-  bool d_single_invocation;
-  // single invocation portion of quantified formula
-  Node d_single_inv;
-  
  public:
   CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s);
   ~CegSingleInv();
 
-  // get simplified conjecture
+  /** Get simplified conjecture. */
   Node getSimplifiedConjecture() { return d_simp_quant; }
   /** initialize this class for synthesis conjecture q */
   void initialize( Node q );
@@ -146,7 +97,33 @@ class CegSingleInv
   /** preregister conjecture */
   void preregisterConjecture( Node q );
 
+  //---------------------------------representation of the solution
+  /**
+   * The list of instantiations that suffice to show the first-order equivalent
+   * of the negated synthesis conjecture is unsatisfiable.
+   */
+  std::vector<std::vector<Node> > d_inst;
+  /**
+   * The list of instantiation lemmas, corresponding to instantiations of the
+   * first order conjecture for the term vectors above.
+   */
+  std::vector<Node> d_instConds;
+  /** The solutions, without reconstruction to syntax */
+  std::vector<Node> d_solutions;
+  /** The solutions, after reconstruction to syntax */
+  std::vector<Node> d_rcSolutions;
+  /** is solved */
+  bool d_isSolved;
+  //---------------------------------end representation of the solution
+
  private:
+  // presolve
+  void collectPresolveEqTerms(Node n, std::map<Node, std::vector<Node> >& teq);
+  void getPresolveEqConjuncts(std::vector<Node>& vars,
+                              std::vector<Node>& terms,
+                              std::map<Node, std::vector<Node> >& teq,
+                              Node n,
+                              std::vector<Node>& conj);
   /** solve trivial
    *
    * If this method returns true, it sets d_isSolved to true and adds
@@ -165,6 +142,25 @@ class CegSingleInv
    * calls to the above method getSolutionFromInst.
    */
   void setSolution();
+
+  // single invocation inference utility
+  SingleInvocationPartition* d_sip;
+  /** solution reconstruction */
+  std::unique_ptr<SygusReconstruct> d_srcons;
+
+  // list of skolems for each argument of programs
+  std::vector<Node> d_single_inv_arg_sk;
+  // program to solution index
+  std::map<Node, unsigned> d_prog_to_sol_index;
+  // original conjecture
+  Node d_orig_conjecture;
+
+  Node d_simp_quant;
+  // are we single invocation?
+  bool d_single_invocation;
+  // single invocation portion of quantified formula
+  Node d_single_inv;
+
   /** Reference to the term registry */
   TermRegistry& d_treg;
   /** The conjecture */