From: Andrew Reynolds Date: Wed, 27 Jan 2021 02:45:26 +0000 (-0600) Subject: Use term canonizer utility locally in quantifiers (#5823) X-Git-Tag: cvc5-1.0.0~2350 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=693ed2fd482791e29e5d86420d0aa2ac835b7260;p=cvc5.git 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 b4f9ee015..643a652e7 100644 --- 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 c2e8e2214..987864317 100644 --- 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 280c8c511..cd363eb70 100644 --- 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; isecond; 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 e45853e12..c73abd19b 100644 --- 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 83aafe33a..94f70a2d9 100644 --- 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 & pattern) { - for(std::vector::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 2790ad11a..d09090da3 100644 --- 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 & pattern); /** assert universal quantifier */ void assertQuantifier( Node q, bool pol ); private: @@ -353,8 +346,6 @@ public: std::unique_ptr d_builder; /** term utilities */ std::unique_ptr d_term_util; - /** term utilities */ - std::unique_ptr d_term_canon; /** term database */ std::unique_ptr d_term_db; /** sygus term database */