Use term canonizer utility locally in quantifiers (#5823)

Term canonization was used in two places, which are unrelated and don't need to share the instance.
Also removes a few unnecessary methods from QuantifiersEngine.

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index b4f9ee01556e5bd68bb184d1895058956d421870..643a652e70693793debc61abbc69a3792017cd65 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -130,7 +130,7 @@ Node AlphaEquivalenceDb::addTerm(Node q)
 }
 
 AlphaEquivalence::AlphaEquivalence(QuantifiersEngine* qe)
-    : d_aedb(qe->getTermCanonize())
+    : d_termCanon(), d_aedb(&d_termCanon)
 {
 }
 

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index c2e8e2214cdc8cf8e23471b93be311c427734968..987864317d131b3779f16d6d358b0990b48c9568 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -114,6 +114,8 @@ class AlphaEquivalence
   Node reduceQuantifier( Node q );
 
  private:
+  /** a term canonizer */
+  expr::TermCanonize d_termCanon;
   /** the database of quantified formulas registered to this class */
   AlphaEquivalenceDb d_aedb;
 };

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 280c8c511ba2977fd50408bd949f3817adec19a5..cd363eb70be90cddeb4294a5c1668b72690df51f 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -312,7 +312,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
 }
 
 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
-  return d_quantEngine->getTermCanonize()->getCanonicalFreeVar(tn, i);
+  return d_termCanon.getCanonicalFreeVar(tn, i);
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
@@ -545,7 +545,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
               if( d_tge.isRelevantTerm( eq ) ){
                 //make it canonical
                 Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
-                eq = d_quantEngine->getTermCanonize()->getCanonicalTerm(eq);
+                eq = d_termCanon.getCanonicalTerm(eq);
               }else{
                 eq = Node::null();
               }
@@ -700,8 +700,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
                 sum += it->second;
                 for( unsigned i=0; i<it->second; i++ ){
                   gsubs_vars.push_back(
-                      d_quantEngine->getTermCanonize()->getCanonicalFreeVar(
-                          it->first, i));
+                      d_termCanon.getCanonicalFreeVar(it->first, i));
                 }
               }
             }

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index e45853e121ca12a71b9275db3a21c2acf3cc90d2..c73abd19b3d35249fe5907c09c529a5f3b02ab76 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -19,6 +19,7 @@
 
 #include "context/cdhashmap.h"
 #include "expr/node_trie.h"
+#include "expr/term_canonize.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/type_enumerator.h"
 
@@ -457,6 +458,8 @@ private:  //information about ground equivalence classes
   unsigned optFullCheckConjectures();
 
   bool optStatsOnly();
+  /** term canonizer */
+  expr::TermCanonize d_termCanon;
 };
 
 

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 83aafe33a778014a62c285334aaea2a5774f6883..94f70a2d91d52b5fe353f7e01e3a0cf8eaf6dfc2 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -44,7 +44,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_model(nullptr),
       d_builder(nullptr),
       d_term_util(new quantifiers::TermUtil),
-      d_term_canon(new expr::TermCanonize),
       d_term_db(new quantifiers::TermDb(qstate, qim, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
@@ -150,11 +149,6 @@ OutputChannel& QuantifiersEngine::getOutputChannel()
 /** get default valuation for the quantifiers engine */
 Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
 
-const LogicInfo& QuantifiersEngine::getLogicInfo() const
-{
-  return d_te->getLogicInfo();
-}
-
 EqualityQuery* QuantifiersEngine::getEqualityQuery() const
 {
   return d_eq_query.get();
@@ -179,10 +173,6 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
 {
   return d_term_util.get();
 }
-expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
-{
-  return d_term_canon.get();
-}
 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
 {
   return d_quant_attr.get();
@@ -773,13 +763,6 @@ void QuantifiersEngine::preRegisterQuantifier(Node q)
   Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
 }
 
-void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
-  for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
-    std::set< Node > added;
-    getTermDatabase()->addTerm( *p, added );
-  }
-}
-
 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   if (reduceQuantifier(f))
   {

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2790ad11a7e9390766da14e8adbee754e01b4467..d09090da395737e7dca7e70c6aed9cce1e0beee5 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -23,7 +23,6 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "expr/attribute.h"
-#include "expr/term_canonize.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -74,8 +73,6 @@ class QuantifiersEngine {
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
-  /** get the logic info for the quantifiers engine */
-  const LogicInfo& getLogicInfo() const;
   //---------------------- end external interface
   //---------------------- utilities
   /** get the master equality engine */
@@ -92,8 +89,6 @@ class QuantifiersEngine {
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
   /** get term utilities */
   quantifiers::TermUtil* getTermUtil() const;
-  /** get term canonizer */
-  expr::TermCanonize* getTermCanonize() const;
   /** get quantifiers attributes */
   quantifiers::QuantAttributes* getQuantAttributes() const;
   /** get instantiate utility */
@@ -191,8 +186,6 @@ class QuantifiersEngine {
    * that are pre-registered to the quantifiers theory.
    */
   void preRegisterQuantifier(Node q);
-  /** register quantifier */
-  void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
   void assertQuantifier( Node q, bool pol );
 private:
@@ -353,8 +346,6 @@ public:
   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
   /** term utilities */
   std::unique_ptr<quantifiers::TermUtil> d_term_util;
-  /** term utilities */
-  std::unique_ptr<expr::TermCanonize> d_term_canon;
   /** term database */
   std::unique_ptr<quantifiers::TermDb> d_term_db;
   /** sygus term database */