Eliminate non-static members in term util (#5919)

This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.

This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.

9 files changed, 20 insertions, 36 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 1748dea8e..b296a4421 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -544,7 +544,8 @@ void CegSingleInvSol::getEquivalentTerms(Kind k,
         }
         if( !eq.isNull() ){
           eq = Rewriter::rewrite( eq );
-          if( eq!=d_qe->getTermUtil()->d_true ){
+          if (!eq.isConst() || !eq.getConst<bool>())
+          {
             success = false;
             break;
           }
@@ -788,7 +789,7 @@ void CegSingleInvSol::registerType(TypeNode tn)
   TypeNode btn = dt.getSygusType();
   // for constant reconstruction
   Kind ck = getComparisonKind(btn);
-  Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
+  Node z = TermUtil::mkTypeValue(btn, 0);
 
   // iterate over constructors
   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 00a72cbcb..538d80e44 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
 
 using namespace CVC4::kind;
@@ -34,9 +33,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe,
+CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds,
                                              SynthConjecture* p)
-    : d_qe(qe), d_parent(p), d_is_syntax_restricted(false)
+    : d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
 {
 }
 
@@ -138,7 +137,7 @@ Node CegGrammarConstructor::process(Node q,
       sfvl = preGrammarType.getDType().getSygusVarList();
       tn = preGrammarType;
       // normalize type, if user-provided
-      SygusGrammarNorm sygus_norm(d_qe);
+      SygusGrammarNorm sygus_norm(d_tds);
       tn = sygus_norm.normalizeSygusType(tn, sfvl);
     }else{
       sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
@@ -205,7 +204,6 @@ Node CegGrammarConstructor::process(Node q,
 
   std::vector<Node> qchildren;
   Node qbody_subs = q[1];
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
   {
     Node sf = q[0][i];
@@ -253,7 +251,7 @@ Node CegGrammarConstructor::process(Node q,
         Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
       }
     }
-    tds->registerSygusType(tn);
+    d_tds->registerSygusType(tn);
     Assert(tn.isDatatype());
     const DType& dt = tn.getDType();
     Assert(dt.isSygus());
@@ -282,7 +280,6 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
   std::stack<TNode> visit;
   TNode cur;
   visit.push(n);
-  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   do {
     cur = visit.top();
     visit.pop();
@@ -347,7 +344,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n)
           //   lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
           // where ef is the first order variable for the
           // function-to-synthesize.
-          SygusTypeInfo& ti = tds->getTypeInfo(ef.getType());
+          SygusTypeInfo& ti = d_tds->getTypeInfo(ef.getType());
           const std::vector<Node>& vars = ti.getVarList();
           Assert(!vars.empty());
           std::vector<Node> vs;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 6edfbebd5..67d5eb027 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -28,8 +28,6 @@
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
 /**
  * Attribute for associating a function-to-synthesize with a first order
  * variable whose type is a sygus datatype type that encodes its grammar.
@@ -53,6 +51,7 @@ typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node>
 namespace quantifiers {
 
 class SynthConjecture;
+class TermDbSygus;
 
 /**
  * Utility for constructing datatypes that correspond to syntactic restrictions,
@@ -61,7 +60,7 @@ class SynthConjecture;
 class CegGrammarConstructor
 {
 public:
- CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p);
+ CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p);
  ~CegGrammarConstructor() {}
  /** process
   *
@@ -169,8 +168,8 @@ public:
   Node convertToEmbedding(Node n);
 
  private:
-  /** reference to quantifier engine */
-  QuantifiersEngine * d_qe;
+  /** The sygus term database we are using */
+  TermDbSygus* d_tds;
   /** parent conjecture
   * This contains global information about the synthesis conjecture.
   */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 644d50a95..7d757ca98 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -25,7 +25,6 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 #include <numeric>  // for std::iota
 
@@ -68,10 +67,7 @@ bool OpPosTrie::getOrMakeType(TypeNode tn,
   return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
 }
 
-SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe)
-    : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus())
-{
-}
+SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {}
 
 SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
     : d_tn(src_tn),
@@ -287,7 +283,7 @@ std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
   if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
   {
     SygusRedundantCons src;
-    src.initialize(d_qe, tn);
+    src.initialize(d_tds, tn);
     std::vector<unsigned> rindices;
     src.getRedundant(rindices);
     if (!rindices.empty())
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 48a5dbe06..2827d2837 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -25,7 +25,6 @@
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
 #include "expr/type_node.h"
-#include "theory/quantifiers/term_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -128,7 +127,7 @@ class OpPosTrie
 class SygusGrammarNorm
 {
  public:
-  SygusGrammarNorm(QuantifiersEngine* qe);
+  SygusGrammarNorm(TermDbSygus* tds);
   ~SygusGrammarNorm() {}
   /** creates a normalized typenode from a given one.
    *
@@ -363,8 +362,6 @@ class SygusGrammarNorm
 
   }; /* class TransfChain */
 
-  /** reference to quantifier engine */
-  QuantifiersEngine* d_qe;
   /** sygus term database associated with this utility */
   TermDbSygus* d_tds;
   /** List of variable inputs of function-to-synthesize.
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index e6b9b3593..6e36222b6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -19,7 +19,6 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -28,13 +27,12 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
+void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
 {
-  Assert(qe != nullptr);
+  Assert(tds != nullptr);
   Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
   d_type = tn;
   Assert(tn.isDatatype());
-  TermDbSygus* tds = qe->getTermDatabaseSygus();
   tds->registerSygusType(tn);
   const DType& dt = tn.getDType();
   Assert(dt.isSygus());
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 7fda6acbe..ace855ee1 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -24,9 +24,6 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
 class TermDbSygus;
@@ -48,7 +45,7 @@ class SygusRedundantCons
    * qe : pointer to the quantifiers engine,
    * tn : the (sygus) type to compute redundant constructors for
    */
-  void initialize(QuantifiersEngine* qe, TypeNode tn);
+  void initialize(TermDbSygus* tds, TypeNode tn);
   /** Get the indices of the redundant constructors of the register type */
   void getRedundant(std::vector<unsigned>& indices);
   /**
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 59edd3070..909a9aecc 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -53,7 +53,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_ceg_si(new CegSingleInv(qe)),
       d_templInfer(new SygusTemplateInfer),
       d_ceg_proc(new SynthConjectureProcess(qe)),
-      d_ceg_gc(new CegGrammarConstructor(qe, this)),
+      d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
       d_exampleInfer(new ExampleInfer(d_tds)),
       d_ceg_pbe(new SygusPbe(qe, this)),
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 728797d85..e800a52cf 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -939,8 +939,7 @@ bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
     if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL || 
         k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
       if( n[1].isConst() ){
-        if (n[1]
-            == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0))
+        if (n[1] == TermUtil::mkTypeValue(n[1].getType(), 0))
         {
           return true;
         }