From 34e84a25a044e3af192bb69089467c2125911900 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 28 Oct 2017 09:13:13 -0500 Subject: [PATCH] Document term db (#1220) * Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206. * Minor * Minor * Change namespace style. * Address review * Fix incorrectly merged portion that led to regression failures. * New clang format, fully document relevant domain. * Clang format again. * Minor --- src/theory/quantifiers/equality_query.cpp | 57 ++- src/theory/quantifiers/equality_query.h | 99 +++-- src/theory/quantifiers/full_model_check.cpp | 8 +- src/theory/quantifiers/inst_propagator.h | 12 +- src/theory/quantifiers/quant_util.h | 137 +++++-- .../quantifiers/quantifiers_attributes.cpp | 30 +- .../quantifiers/quantifiers_attributes.h | 63 ++- src/theory/quantifiers/relevant_domain.cpp | 8 +- src/theory/quantifiers/relevant_domain.h | 119 +++++- src/theory/quantifiers/term_database.cpp | 18 +- src/theory/quantifiers/term_database.h | 376 +++++++++++++----- src/theory/quantifiers/term_util.h | 15 +- src/theory/quantifiers_engine.cpp | 38 +- src/theory/quantifiers_engine.h | 22 +- src/theory/theory.h | 3 +- 15 files changed, 745 insertions(+), 260 deletions(-) diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index fb8ac4195..e79f3456b 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -23,11 +23,12 @@ #include "theory/uf/equality_engine.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){ @@ -116,8 +117,11 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } } -Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ - Assert( f.isNull() || f.getKind()==FORALL ); +Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, + Node q, + int index) +{ + Assert(q.isNull() || q.getKind() == FORALL); Node r = getRepresentative( a ); if( options::finiteModelFind() ){ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ @@ -141,27 +145,38 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ return r; }else{ - TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); - std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); - if( itir==d_int_rep[v_tn].end() ){ + TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); + std::map& v_int_rep = d_int_rep[v_tn]; + std::map::const_iterator itir = v_int_rep.find(r); + if (itir != v_int_rep.end()) + { + return itir->second; + } + else + { //find best selection for representative Node r_best; - //if( options::fmfRelevantDomain() && !f.isNull() ){ - // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl; - // r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r ); - // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl; + // if( options::fmfRelevantDomain() && !q.isNull() ){ + // Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << + // r << std::endl; + // r_best = d_qe->getRelevantDomain()->getRelevantTerm( q, index, r ); + // Trace("internal-rep-debug") << "Returned " << r_best << " " << r << + // std::endl; //} std::vector< Node > eqc; getEquivalenceClass( r, eqc ); Trace("internal-rep-select") << "Choose representative for equivalence class : { "; for( unsigned i=0; i0 ) Trace("internal-rep-select") << ", "; + if (i > 0) + { + Trace("internal-rep-select") << ", "; + } Trace("internal-rep-select") << eqc[i]; } Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; int r_best_score = -1; for( size_t i=0; i=0 && ( r_best_score<0 || scoresecond; } } } @@ -311,7 +324,11 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){ +int EqualityQueryQuantifiersEngine::getRepScore(Node n, + Node q, + int index, + TypeNode v_tn) +{ if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type @@ -335,3 +352,7 @@ int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, Type } } } + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index c3e0a8c5b..0048cc14f 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -17,17 +17,87 @@ #ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H #define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { -// TODO : (as part of #1171, #1214) further document and clean this class. -/** equality query object using theory engine */ +/** EqualityQueryQuantifiersEngine class +* This is a wrapper class around an equality engine that is used for +* queries required by algorithms in the quantifiers theory. +* It uses an equality engine, as determined by the quantifiers engine it points +* to. +* +* The main extension of this class wrt EqualityQuery is the function +* getInternalRepresentative, which is used by instantiation-based methods +* that are agnostic with respect to choosing terms within an equivalence class. +* Examples of such methods are finite model finding and enumerative +* instantiation. +* Method getInternalRepresentative returns the "best" representative based on +* the internal heuristic, +* which is currently based on choosing the term that was previously chosen as a +* representative +* earliest. +*/ class EqualityQueryQuantifiersEngine : public EqualityQuery { -private: + public: + EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe); + virtual ~EqualityQueryQuantifiersEngine(); + /** reset */ + virtual bool reset(Theory::Effort e); + /* Called for new quantifiers */ + virtual void registerQuantifier(Node q) {} + /** identify */ + virtual std::string identify() const { return "EqualityQueryQE"; } + /** does the equality engine have term a */ + bool hasTerm(Node a); + /** get the representative of a */ + Node getRepresentative(Node a); + /** are a and b equal? */ + bool areEqual(Node a, Node b); + /** are a and b disequal? */ + bool areDisequal(Node a, Node b); + /** get equality engine + * This may either be the master equality engine or the model's equality + * engine. + */ + eq::EqualityEngine* getEngine(); + /** get list of members in the equivalence class of a */ + void getEquivalenceClass(Node a, std::vector& eqc); + /** get congruent term + * If possible, returns a term n such that: + * (1) n is a term in the equality engine from getEngine(). + * (2) n is of the form f( t1, ..., tk ) where ti is in the equivalence class + * of args[i] for i=1...k + * Otherwise, returns the null node. + * + * Notice that f should be a "match operator", returned by + * TermDb::getMatchOperator. + */ + TNode getCongruentTerm(Node f, std::vector& args); + /** gets the current best representative in the equivalence + * class of a, based on some heuristic. Currently, the default heuristic + * chooses terms that were previously chosen as representatives + * on the earliest instantiation round. + * + * If q is non-null, then q/index is the quantified formula + * and variable position that we are choosing for instantiation. + * + * This function avoids certain terms that are "ineligible" for instantiation. + * If cbqi is active, we terms that contain instantiation constants + * are ineligible. As a result, this function may return + * Node::null() if all terms in the equivalence class of a + * are ineligible. + */ + Node getInternalRepresentative(Node a, Node q, int index); + + private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** quantifiers equality inference */ @@ -36,9 +106,8 @@ private: std::map< TypeNode, std::map< Node, Node > > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; - /** reset count */ + /** the number of times reset( e ) has been called */ int d_reset_count; - /** processInferences : will merge equivalence classes in master equality engine, if possible */ bool processInferences( Theory::Effort e ); /** node contains */ @@ -47,26 +116,6 @@ private: int getRepScore( Node n, Node f, int index, TypeNode v_tn ); /** flatten representatives */ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); -public: - EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ); - virtual ~EqualityQueryQuantifiersEngine(); - /** reset */ - bool reset( Theory::Effort e ); - /** identify */ - std::string identify() const { return "EqualityQueryQE"; } - /** general queries about equality */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - eq::EqualityEngine* getEngine(); - void getEquivalenceClass( Node a, std::vector< Node >& eqc ); - TNode getCongruentTerm( Node f, std::vector< TNode >& args ); - /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria. - If cbqi is active, this will return a term in the equivalence class of "a" that does - not contain instantiation constants, if such a term exists. - */ - Node getInternalRepresentative( Node a, Node f, int index ); }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index db43d8bca..b0f118ad5 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -30,9 +30,10 @@ using namespace CVC4::theory::quantifiers::fmcheck; struct ModelBasisArgSort { std::vector< Node > d_terms; + // number of arguments that are model-basis terms + std::unordered_map d_mba_count; bool operator() (int i,int j) { - return (d_terms[i].getAttribute(ModelBasisArgAttribute()) < - d_terms[j].getAttribute(ModelBasisArgAttribute()) ); + return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]); } }; @@ -502,8 +503,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ std::vector< int > indices; ModelBasisArgSort mbas; for (int i=0; i<(int)conds.size(); i++) { - d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] ); mbas.d_terms.push_back(conds[i]); + mbas.d_mba_count[conds[i]] = + d_qe->getTermDatabase()->getModelBasisArg(conds[i]); indices.push_back(i); } std::sort( indices.begin(), indices.end(), mbas ); diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 6c058c258..580923fc9 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -38,9 +38,11 @@ public: EqualityQueryInstProp( QuantifiersEngine* qe ); ~EqualityQueryInstProp(){}; /** reset */ - bool reset( Theory::Effort e ); + virtual bool reset(Theory::Effort e); + /* Called for new quantifiers */ + virtual void registerQuantifier(Node q) {} /** identify */ - std::string identify() const { return "EqualityQueryInstProp"; } + virtual std::string identify() const { return "EqualityQueryInstProp"; } /** extends engine */ bool extendsEngine() { return true; } /** contains term */ @@ -161,9 +163,11 @@ public: InstPropagator( QuantifiersEngine* qe ); ~InstPropagator(){} /** reset */ - bool reset( Theory::Effort e ); + virtual bool reset(Theory::Effort e) override; + /* Called for new quantifiers */ + virtual void registerQuantifier(Node q) override {} /** identify */ - std::string identify() const { return "InstPropagator"; } + virtual std::string identify() const override { return "InstPropagator"; } /** get the notify mechanism */ InstantiationNotify* getInstantiationNotify() { return &d_notify; } }; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 07df8bb21..ad6ab509d 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -19,6 +19,7 @@ #include #include +#include #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -33,52 +34,129 @@ namespace quantifiers { class TermUtil; } +/** QuantifiersModule class +* +* This is the virtual class for defining subsolvers of the quantifiers theory. +* It has a similar interface to a Theory object. +*/ class QuantifiersModule { -protected: - QuantifiersEngine* d_quantEngine; public: QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} virtual ~QuantifiersModule(){} - //get quantifiers engine - QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } - /** presolve */ + /** Presolve. + * + * Called at the beginning of check-sat call. + */ virtual void presolve() {} - /* whether this module needs to check this round */ + /** Needs check. + * + * Returns true if this module wishes a call to be made + * to check(e) during QuantifiersEngine::check(e). + */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } - /* whether this module needs a model built */ + /** Needs model. + * + * Whether this module needs a model built during a + * call to QuantifiersEngine::check(e) + * It returns one of QEFFORT_* from quantifiers_engine.h, + * which specifies the quantifiers effort in which it requires the model to + * be built. + */ virtual unsigned needsModel( Theory::Effort e ); - /* reset at a round */ + /** Reset. + * + * Called at the beginning of QuantifiersEngine::check(e). + */ virtual void reset_round( Theory::Effort e ){} - /* Call during quantifier engine's check */ + /** Check. + * + * Called during QuantifiersEngine::check(e) depending + * if needsCheck(e) returns true. + */ virtual void check( Theory::Effort e, unsigned quant_e ) = 0; - /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */ + /** Check complete? + * + * Returns false if the module's reasoning was globally incomplete + * (e.g. "sat" must be replaced with "incomplete"). + * + * This is called just before the quantifiers engine will return + * with no lemmas added during a LAST_CALL effort check. + */ virtual bool checkComplete() { return true; } - /* check was complete for quantified formula q (e.g. no lemmas implies a model) */ + /** Check was complete for quantified formula q + * + * If for each quantified formula q, some module returns true for + * checkCompleteFor( q ), + * and no lemmas are added by the quantifiers theory, then we may answer + * "sat", unless + * we are incomplete for other reasons. + */ virtual bool checkCompleteFor( Node q ) { return false; } - /* Called for new quantified formulas */ + /** Pre register quantifier. + * + * Called once for new quantified formulas that are + * pre-registered by the quantifiers theory. + */ virtual void preRegisterQuantifier( Node q ) { } - /* Called for new quantifiers after owners are finalized */ + /** Register quantifier + * + * Called once for new quantified formulas that are + * pre-registered by the quantifiers theory, after + * internal ownership of quantified formulas is finalized. + */ virtual void registerQuantifier( Node q ) = 0; - virtual void assertNode( Node n ) {} - virtual void propagate( Theory::Effort level ){} + /** Assert node. + * + * Called when a quantified formula q is asserted to the quantifiers theory + */ + virtual void assertNode(Node q) {} + /* Get the next decision request. + * + * Identical to Theory::getNextDecisionRequest(...) + */ virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); } /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; -public: + //----------------------------general queries + /** get currently used the equality engine */ eq::EqualityEngine * getEqualityEngine(); - bool areDisequal( TNode n1, TNode n2 ); + /** are n1 and n2 equal in the current used equality engine? */ bool areEqual( TNode n1, TNode n2 ); + /** are n1 and n2 disequal in the current used equality engine? */ + bool areDisequal(TNode n1, TNode n2); + /** get the representative of n in the current used equality engine */ TNode getRepresentative( TNode n ); + /** get quantifiers engine that owns this module */ + QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + /** get currently used term database */ quantifiers::TermDb * getTermDatabase(); + /** get currently used term utility object */ quantifiers::TermUtil * getTermUtil(); + //----------------------------end general queries + protected: + /** pointer to the quantifiers engine that owns this module */ + QuantifiersEngine* d_quantEngine; };/* class QuantifiersModule */ +/** Quantifiers utility +* +* This is a lightweight version of a quantifiers module that does not implement +* methods +* for checking satisfiability. +*/ class QuantifiersUtil { public: QuantifiersUtil(){} virtual ~QuantifiersUtil(){} - /* reset at a round */ + /* reset + * Called at the beginning of an instantiation round + * Returns false if the reset failed. When reset fails, the utility should have + * added a lemma + * via a call to qe->addLemma. TODO: improve this contract #1163 + */ virtual bool reset( Theory::Effort e ) = 0; + /* Called for new quantifiers */ + virtual void registerQuantifier(Node q) = 0; /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; }; @@ -238,8 +316,12 @@ public: static void debugPrintMonomialSum(std::map& msum, const char* c); }; - -class QuantRelevance +/** QuantRelevance +* This class is used for implementing SinE-style heuristics (e.g. see Hoder et +* al CADE 2011) +* This is enabled by the option --relevant-triggers. +*/ +class QuantRelevance : public QuantifiersUtil { private: /** for computing relevance */ @@ -255,8 +337,12 @@ private: public: QuantRelevance( bool cr ) : d_computeRel( cr ){} ~QuantRelevance(){} - /** register quantifier */ - void registerQuantifier( Node f ); + virtual bool reset(Theory::Effort e) override { return true; } + /** Called for new quantifiers after ownership of quantified formulas are + * finalized */ + virtual void registerQuantifier(Node q) override; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const override { return "QuantRelevance"; } /** set relevance */ void setRelevance( Node s, int r ); /** get relevance */ @@ -288,7 +374,9 @@ public: static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); }; - +/** EqualityQuery +* This is a wrapper class around equality engine. +*/ class EqualityQuery : public QuantifiersUtil { public: EqualityQuery(){} @@ -307,7 +395,8 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; - /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */ + /** get the term that exists in EE that is congruent to f with args (f is + * returned by TermDb::getMatchOperator(...)) */ virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index c9a7f07ab..d02ad667e 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -22,11 +22,12 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : d_quantEngine(qe) { @@ -94,7 +95,10 @@ bool QuantAttributes::checkRewriteRule( Node q ) { } Node QuantAttributes::getRewriteRule( Node q ) { - if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){ + if (q.getKind() == FORALL && q.getNumChildren() == 3 + && q[2][0].getNumChildren() > 0 + && q[2][0][0].getKind() == REWRITE_RULE) + { return q[2][0][0]; }else{ return Node::null(); @@ -121,12 +125,13 @@ bool QuantAttributes::checkFunDefAnnotation( Node ipl ) { Node QuantAttributes::getFunDefHead( Node q ) { //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF && if( q.getKind()==FORALL && q.getNumChildren()==3 ){ - - for( unsigned i=0; isetOwner( q, d_quantEngine->getFunDefEngine(), 2 ); @@ -383,3 +388,6 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) { } } +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 1c35b646b..b618fc5d5 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -61,34 +61,53 @@ namespace quantifiers { //struct RrPriorityAttributeId {}; //typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; - -/** This class stores attributes for quantified formulas -* TODO : document (as part of #1171, #1215) -*/ -class QAttributes{ -public: +/** This struct stores attributes for a single quantified formula */ +struct QAttributes +{ + public: QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} ~QAttributes(){} + /** does the quantified formula have a pattern? */ bool d_hasPattern; + /** if non-null, this is the rewrite rule representation of the quantified + * formula */ Node d_rr; + /** is this formula marked a conjecture? */ bool d_conjecture; + /** is this formula marked an axiom? */ bool d_axiom; + /** if non-null, this quantified formula is a function definition for function + * d_fundef_f */ Node d_fundef_f; + /** is this formula marked as a sygus conjecture? */ bool d_sygus; + /** is this formula marked as a synthesis (non-sygus) conjecture? */ bool d_synthesis; + /** if a rewrite rule, then this is the priority value for the rewrite rule */ int d_rr_priority; + /** stores the maximum instantiation level allowed for this quantified formula + * (-1 means allow any) */ int d_qinstLevel; + /** is this formula marked for quantifier elimination? */ bool d_quant_elim; + /** is this formula marked for partial quantifier elimination? */ bool d_quant_elim_partial; + /** the instantiation pattern list for this quantified formula (its 3rd child) + */ Node d_ipl; + /** the quantifier id associated with this formula */ Node d_qid_num; + /** is this quantified formula a rewrite rule? */ bool isRewriteRule() { return !d_rr.isNull(); } + /** is this quantified formula a function definition? */ bool isFunDef() { return !d_fundef_f.isNull(); } }; -/** This class caches information about attributes of quantified formulas -* It also has static utility functions used for determining attributes and information about +/** This class caches information about attributes of quantified formulas +* +* It also has static utility functions used for determining attributes and +* information about * quantified formulas. */ class QuantAttributes @@ -96,14 +115,23 @@ class QuantAttributes public: QuantAttributes( QuantifiersEngine * qe ); ~QuantAttributes(){} - /** set user attribute - * This function will apply a custom set of attributes to all top-level universal - * quantifiers contained in n - */ - static void setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ); - - //general queries concerning quantified formulas wrt modules + * This function applies an attribute + * This can be called when we mark expressions with attributes, e.g. (! q + * :attribute attr [node_values, str_value...]), + * It can also be called internally in various ways (for SyGus, quantifier + * elimination, etc.) + */ + static void setUserAttribute(const std::string& attr, + Node q, + std::vector& node_values, + std::string str_value); + + /** compute quantifier attributes */ + static void computeQuantAttributes(Node q, QAttributes& qa); + /** compute the attributes for q */ + void computeAttributes(Node q); + /** is quantifier treated as a rewrite rule? */ static bool checkRewriteRule( Node q ); /** get the rewrite rule associated with the quanfied formula */ @@ -145,10 +173,7 @@ public: int getQuantIdNum( Node q ); /** get quant id num */ Node getQuantIdNumNode( Node q ); - /** compute quantifier attributes */ - static void computeQuantAttributes( Node q, QAttributes& qa ); - /** compute the attributes for q */ - void computeAttributes( Node q ); + private: /** pointer to quantifiers engine */ QuantifiersEngine * d_quantEngine; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 749026b66..dcd24b433 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -98,6 +98,7 @@ bool RelevantDomain::reset( Theory::Effort e ) { return true; } +void RelevantDomain::registerQuantifier(Node q) {} void RelevantDomain::compute(){ if( !d_is_computed ){ d_is_computed = true; @@ -116,11 +117,12 @@ void RelevantDomain::compute(){ Trace("rel-dom-debug") << "account for ground terms" << std::endl; TermDb * db = d_qe->getTermDatabase(); - for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ - Node op = it->first; + for (unsigned k = 0; k < db->getNumOperators(); k++) + { + Node op = db->getOperator(k); unsigned sz = db->getNumGroundTerms( op ); for( unsigned i=0; isecond[i]; + Node n = db->getGroundTerm(op, i); //if it is a non-redundant term if( db->isTermActive( n ) ){ for( unsigned j=0; j d_terms; + /** reset this object */ + void reset() + { + d_parent = NULL; + d_terms.clear(); + } + /** merge this with r + * This sets d_parent of this to r and + * copies the terms of this to r. + */ void merge( RDomain * r ); + /** add term to the relevant domain */ void addTerm( Node t ); + /** get the parent of this */ RDomain * getParent(); + /** remove redundant terms for d_terms, removes + * duplicates modulo equality. + */ void removeRedundantTerms( QuantifiersEngine * qe ); + /** is n in this relevant domain? */ bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } + + private: + /** the parent of this relevant domain */ + RDomain* d_parent; }; + /** get the relevant domain + * + * Gets object representing the relevant domain of the i^th argument of n. + * + * If getParent is true, we return the representative + * of the equivalence class of relevant domain objects, + * which is computed as a union find (see RDomain::d_parent). + */ + RDomain* getRDomain(Node n, int i, bool getParent = true); + + private: + /** the relevant domains for each quantified formula and function, + * for each variable # and argument #. + */ std::map< Node, std::map< int, RDomain * > > d_rel_doms; + /** stores the function or quantified formula associated with + * each relevant domain object. + */ std::map< RDomain *, Node > d_rn_map; + /** stores the argument or variable number associated with + * each relevant domain object. + */ std::map< RDomain *, int > d_ri_map; + /** Quantifiers engine associated with this utility. */ QuantifiersEngine* d_qe; - void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ); - void computeRelevantDomainOpCh( RDomain * rf, Node n ); + /** have we computed the relevant domain on this full effort check? */ bool d_is_computed; - - //what each literal does + /** relevant domain literal + * Caches the effect of literals on the relevant domain. + */ class RDomainLit { public: RDomainLit() : d_merge(false){ @@ -55,23 +128,33 @@ private: d_rd[1] = NULL; } ~RDomainLit(){} + /** whether this literal forces the merge of two relevant domains */ bool d_merge; + /** the relevant domains that are merged as a result + * of this literal + */ RDomain * d_rd[2]; + /** the terms that are added to + * the relevant domain as a result of this literal + */ std::vector< Node > d_val; }; + /** Cache of the effect of literals on the relevant domain */ std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit; + /** Compute the relevant domain for a subformula n of q, + * whose polarity is given by hasPol/pol. + */ + void computeRelevantDomain(Node q, Node n, bool hasPol, bool pol); + /** Compute the relevant domain when the term n + * is in a position to be included in relevant domain rf. + */ + void computeRelevantDomainOpCh(RDomain* rf, Node n); + /** compute relevant domain for literal. + * + * Updates the relevant domains based on a literal n in quantified + * formula q whose polarity is given by hasPol/pol. + */ void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ); -public: - RelevantDomain( QuantifiersEngine* qe ); - virtual ~RelevantDomain(); - /* reset */ - bool reset( Theory::Effort e ); - /** identify */ - std::string identify() const { return "RelevantDomain"; } - //compute the relevant domain - void compute(); - - RDomain * getRDomain( Node n, int i, bool getParent = true ); };/* class RelevantDomain */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d4a71e43c..59405a5d5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -104,6 +104,13 @@ void TermDb::registerQuantifier( Node q ) { } } +unsigned TermDb::getNumOperators() { return d_ops.size(); } +Node TermDb::getOperator(unsigned i) +{ + Assert(i < d_ops.size()); + return d_ops[i]; +} + /** ground terms */ unsigned TermDb::getNumGroundTerms( Node f ) { std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); @@ -178,6 +185,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi Node op = getMatchOperator( n ); Trace("term-db-debug") << " match operator is : " << op << std::endl; + d_ops.push_back(op); d_op_map[op].push_back( n ); added.insert( n ); @@ -720,7 +728,9 @@ void TermDb::setHasTerm( Node n ) { void TermDb::presolve() { if( options::incrementalSolving() ){ - //reset the caches that are SAT context-independent + // reset the caches that are SAT context-independent but user + // context-dependent + d_ops.clear(); d_op_map.clear(); d_type_map.clear(); d_processed.clear(); @@ -969,6 +979,12 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ } } +unsigned TermDb::getModelBasisArg(Node n) +{ + computeModelBasisArgAttribute(n); + return n.getAttribute(ModelBasisArgAttribute()); +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f4c6c3877..c5165ec2c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -37,18 +37,65 @@ namespace inst{ namespace quantifiers { +/** Term arg trie class +* +* This also referred to as a "term index" or a "signature table". +* +* This data structure stores a set expressions, indexed by representatives of +* their arguments. +* +* For example, consider the equivalence classes : +* +* { a, d, f( d, c ), f( a, c ) } +* { b, f( b, d ) } +* { c, f( b, b ) } +* +* where the first elements ( a, b, c ) are the representatives of these classes. +* The TermArgTrie t we may build for f is : +* +* t : +* t.d_data[a] : +* t.d_data[a].d_data[c] : +* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf) +* t.d_data[b] : +* t.d_data[b].d_data[b] : +* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf) +* t.d_data[b].d_data[d] : +* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf) +* +* Leaf nodes store the terms that are indexed by the arguments, for example +* term f(d,c) is indexed by the representative arguments (a,c), and is stored +* as a the (single) key in the data of t.d_data[a].d_data[c]. +*/ class TermArgTrie { public: /** the data */ std::map< TNode, TermArgTrie > d_data; public: - bool hasNodeData() { return !d_data.empty(); } - TNode getNodeData() { return d_data.begin()->first; } - TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 ); - TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); - bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 ); - void debugPrint( const char * c, Node n, unsigned depth = 0 ); - void clear() { d_data.clear(); } + /** for leaf nodes : does this trie have data? */ + bool hasNodeData() { return !d_data.empty(); } + /** for leaf nodes : get term corresponding to this leaf */ + TNode getNodeData() { return d_data.begin()->first; } + /** exists term + * Returns the term that is indexed by reps, if one exists, or + * or returns null otherwise. + */ + TNode existsTerm(std::vector& reps, int argIndex = 0); + /** add or get term + * Returns the term that is previously indexed by reps, if one exists, or + * Adds n to the trie, indexed by reps, and returns n. + */ + TNode addOrGetTerm(TNode n, std::vector& reps, int argIndex = 0); + /** add term + * Returns false if a term is previously indexed by reps. + * Returns true if no term is previously indexed by reps, + * and adds n to the trie, indexed by reps, and returns n. + */ + bool addTerm(TNode n, std::vector& reps, int argIndex = 0); + /** debug print this trie */ + void debugPrint(const char* c, Node n, unsigned depth = 0); + /** clear all data from this trie */ + void clear() { d_data.clear(); } };/* class TermArgTrie */ namespace fmcheck { @@ -62,19 +109,199 @@ class ConjectureGenerator; class TermGenerator; class TermGenEnv; +/** Term Database +* +* The primary responsibilities for this class are to : +* (1) Maintain a list of all ground terms that exist in the quantifier-free +* solvers, as notified through the master equality engine. +* (2) Build TermArgTrie objects that index all ground terms, per operator. This +* is done lazily, for performance reasons. +*/ class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; - //TODO: eliminate most of these - friend class ::CVC4::theory::inst::Trigger; - friend class ::CVC4::theory::inst::HigherOrderTrigger; - friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; - friend class ::CVC4::theory::quantifiers::QuantConflictFind; - friend class ::CVC4::theory::quantifiers::RelevantDomain; + // TODO: eliminate these friend class ::CVC4::theory::quantifiers::ConjectureGenerator; friend class ::CVC4::theory::quantifiers::TermGenEnv; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeBoolMap; -private: + + public: + TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); + ~TermDb(); + /** presolve (called once per user check-sat) */ + void presolve(); + /** reset (calculate which terms are active) */ + virtual bool reset(Theory::Effort effort) override; + /** register quantified formula */ + virtual void registerQuantifier(Node q) override; + /** identify */ + virtual std::string identify() const override { return "TermDb"; } + /** get number of operators */ + unsigned getNumOperators(); + /** get operator at index i */ + Node getOperator(unsigned i); + /** ground terms for operator + * Get the number of ground terms with operator f that have been added to the + * database + */ + unsigned getNumGroundTerms(Node f); + /** get ground term for operator + * Get the i^th ground term with operator f that has been added to the database + */ + Node getGroundTerm(Node f, unsigned i); + /** get num type terms + * Get the number of ground terms of tn that have been added to the database + */ + unsigned getNumTypeGroundTerms(TypeNode tn); + /** get type ground term + * Returns the i^th ground term of type tn + */ + Node getTypeGroundTerm(TypeNode tn, unsigned i); + /** add a term to the database + * withinQuant is whether n is within the body of a quantified formula + * withinInstClosure is whether n is within an inst-closure operator (see + * Bansal et al CAV 2015). + */ + void addTerm(Node n, + std::set& added, + bool withinQuant = false, + bool withinInstClosure = false); + /** get match operator for term n + * + * If n has a kind that we index, this function will + * typically return n.getOperator(). + * + * However, for parametric operators f, the match operator is an arbitrary + * chosen f-application. For example, consider array select: + * A : (Array Int Int) + * B : (Array Bool Int) + * We require that terms like (select A 1) and (select B 2) are indexed in + * separate + * data structures despite the fact that + * (select A 1).getOperator()==(select B 2).getOperator(). + * Hence, for the above terms, we may return: + * getMatchOperator( (select A 1) ) = (select A 1), and + * getMatchOperator( (select B 2) ) = (select B 2). + * The match operator is the first instance of an application of the parametric + * operator of its type. + * + * If n has a kind that we do not index (like PLUS), + * then this function returns Node::null(). + */ + Node getMatchOperator(Node n); + /** get term arg index for all f-applications in the current context */ + TermArgTrie* getTermArgTrie(Node f); + /** get the term arg trie for f-applications in the equivalence class of eqc. + */ + TermArgTrie* getTermArgTrie(Node eqc, Node f); + /** get congruent term + * If possible, returns a term t such that: + * (1) t is a term that is currently indexed by this database, + * (2) t is of the form f( t1, ..., tk ) + */ + TNode getCongruentTerm(Node f, Node n); + /** get congruent term + * If possible, returns a term t such that: + * (1) t is a term that is currently indexed by this database, + * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ), + * where ti is in the equivalence class of si for i=1...k + */ + TNode getCongruentTerm(Node f, std::vector& args); + /** in relevant domain + * Returns true if there is at least one term t such that: + * (1) t is a term that is currently indexed by this database, + * (2) t is of the form f( t1, ..., tk ) and ti is in the equivalence class of + * r. + */ + bool inRelevantDomain(TNode f, unsigned i, TNode r); + /** evaluate term + * + * Returns a term n' such that n = n' is entailed based on the equality + * information qy. This function may generate new terms. In particular, + * we typically rewrite maximal + * subterms of n to terms that exist in the equality engine specified by qy. + * + * useEntailmentTests is whether to use the theory engine's entailmentCheck + * call, for increased precision. This is not frequently used. + */ + Node evaluateTerm(TNode n, + EqualityQuery* qy = NULL, + bool useEntailmentTests = false); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by qy), + * (2) n = n' is entailed in the current context. + * It returns null if no such term can be found. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by qy), + * (2) n * subs = n' is entailed in the current context, where * is denotes + * substitution application. + * It returns null if no such term can be found. + * subsRep is whether the substitution maps to terms that are representatives + * according to qy. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, + std::map& subs, + bool subsRep, + EqualityQuery* qy = NULL); + /** is entailed + * Checks whether the current context entails n with polarity pol, based on the + * equality information qy. + * Returns true if the entailment can be successfully shown. + */ + bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL); + /** is entailed + * + * Checks whether the current context entails ( n * subs ) with polarity pol, + * based on the equality information qy, + * where * denotes substitution application. + * subsRep is whether the substitution maps to terms that are representatives + * according to qy. + */ + bool isEntailed(TNode n, + std::map& subs, + bool subsRep, + bool pol, + EqualityQuery* qy = NULL); + /** is the term n active in the current context? + * + * By default, all terms are active. A term is inactive if: + * (1) it is congruent to another term + * (2) it is irrelevant based on the term database mode. This includes terms + * that only appear in literals that are not relevant. + * (3) it contains instantiation constants (used for CEGQI and cannot be used + * in instantiation). + * (4) it is explicitly set inactive by a call to setTermInactive(...). + * We store whether a term is inactive in a SAT-context-dependent map. + */ + bool isTermActive(Node n); + /** set that term n is inactive in this context. */ + void setTermInactive(Node n); + /** has term current + * + * This function is used in cases where we restrict which terms appear in the + * database, such as for heuristics used in local theory extensions + * and for --term-db-mode=relevant. + * It returns whether the term n should be indexed in the current context. + */ + bool hasTermCurrent(Node n, bool useMode = true); + /** is term eligble for instantiation? */ + bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false); + /** get eligible term in equivalence class */ + Node getEligibleTermInEqc(TNode r); + /** is inst closure */ + bool isInstClosure(Node r); + + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; /** terms processed */ @@ -88,30 +315,17 @@ private: /** boolean terms */ Node d_true; Node d_false; -public: - TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); - ~TermDb(); - - /** register quantified formula */ - void registerQuantifier( Node q ); -public: - /** presolve (called once per user check-sat) */ - void presolve(); - /** reset (calculate which terms are active) */ - bool reset( Theory::Effort effort ); - /** identify */ - std::string identify() const { return "TermDb"; } -private: + /** list of all operators */ + std::vector d_ops; /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; /** inactive map */ NodeBoolMap d_inactive_map; - - /** count number of non-redundant ground terms per operator */ + /** count of the number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; - /**mapping from UF terms to representatives of their arguments */ + /** mapping from terms to representatives of their arguments */ std::map< TNode, std::vector< TNode > > d_arg_reps; /** map from operators to trie */ std::map< Node, TermArgTrie > d_func_map_trie; @@ -124,88 +338,58 @@ private: std::map< Node, Node > d_term_elig_eqc; /** set has term */ void setHasTerm( Node n ); - /** evaluate term */ + /** helper for evaluate term */ Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ); + /** helper for get entailed term */ TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + /** helper for is entailed */ bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); - /** compute uf eqc terms */ + /** compute uf eqc terms : + * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes + */ void computeUfEqcTerms( TNode f ); - /** compute uf terms */ + /** compute uf terms + * Ensure that an entry for f is in d_func_map_trie + */ void computeUfTerms( TNode f ); -private: // for higher-order term indexing + /** compute arg reps + * Ensure that an entry for n is in d_arg_reps + */ + void computeArgReps(TNode n); + //------------------------------higher-order term indexing /** a map from matchable operators to their representative */ std::map< TNode, TNode > d_ho_op_rep; /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves; /** get operator representative */ Node getOperatorRepresentative( TNode op ) const; -public: - /** ground terms for operator */ - unsigned getNumGroundTerms( Node f ); - /** get ground term for operator */ - Node getGroundTerm( Node f, unsigned i ); - /** get num type terms */ - unsigned getNumTypeGroundTerms( TypeNode tn ); - /** get type ground term */ - Node getTypeGroundTerm( TypeNode tn, unsigned i ); - /** add a term to the database */ - void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false ); - /** get match operator */ - Node getMatchOperator( Node n ); - /** get term arg index */ - TermArgTrie * getTermArgTrie( Node f ); - TermArgTrie * getTermArgTrie( Node eqc, Node f ); - /** exists term */ - TNode getCongruentTerm( Node f, Node n ); - TNode getCongruentTerm( Node f, std::vector< TNode >& args ); - /** compute arg reps */ - void computeArgReps( TNode n ); - /** in relevant domain */ - bool inRelevantDomain( TNode f, unsigned i, TNode r ); - /** evaluate a term under a substitution. Return representative in EE if possible. - * subsRep is whether subs contains only representatives - */ - Node evaluateTerm( TNode n, EqualityQuery * qy = NULL, bool useEntailmentTests = false ); - /** get entailed term, does not construct new terms, less aggressive */ - TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL ); - TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL ); - /** is entailed (incomplete check) */ - bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL ); - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); - /** is active */ - bool isTermActive( Node n ); - void setTermInactive( Node n ); - /** has term */ - bool hasTermCurrent( Node n, bool useMode = true ); - /** is term eligble for instantiation? */ - bool isTermEligibleForInstantiation( TNode n, TNode f, bool print = false ); - /** get has term eqc */ - Node getEligibleTermInEqc( TNode r ); - /** is inst closure */ - bool isInstClosure( Node r ); - -//for model basis -private: - //map from types to model basis terms + //------------------------------end higher-order term indexing + + // TODO : as part of #1171, these should be moved somewhere else + // for model basis + private: + /** map from types to model basis terms */ std::map< TypeNode, Node > d_model_basis_term; - //map from ops to model basis terms + /** map from ops to model basis terms */ std::map< Node, Node > d_model_basis_op_term; - //map from instantiation terms to their model basis equivalent + /** map from instantiation terms to their model basis equivalent */ std::map< Node, Node > d_model_basis_body; /** map from universal quantifiers to model basis terms */ std::map< Node, std::vector< Node > > d_model_basis_terms; - // compute model basis arg + /** compute model basis arg */ void computeModelBasisArgAttribute( Node n ); -public: - //get model basis term - Node getModelBasisTerm( TypeNode tn, int i = 0 ); - //get model basis term for op - Node getModelBasisOpTerm( Node op ); - //get model basis - Node getModelBasis( Node q, Node n ); - //get model basis body - Node getModelBasisBody( Node q ); - + public: + /** get model basis term */ + Node getModelBasisTerm(TypeNode tn, int i = 0); + /** get model basis term for op */ + Node getModelBasisOpTerm(Node op); + /** get model basis */ + Node getModelBasis(Node q, Node n); + /** get model basis body */ + Node getModelBasisBody(Node q); + /** get model basis arg */ + unsigned getModelBasisArg(Node n); + };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index a0b3b8ec2..f5cfd6df8 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -21,6 +21,7 @@ #include #include "expr/attribute.h" +#include "theory/quantifiers/quant_util.h" #include "theory/type_enumerator.h" namespace CVC4 { @@ -109,7 +110,8 @@ namespace quantifiers { class TermDatabase; // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. -class TermUtil { +class TermUtil : public QuantifiersUtil +{ // TODO : remove these friend class ::CVC4::theory::QuantifiersEngine; friend class TermDatabase; @@ -126,11 +128,14 @@ public: Node d_zero; Node d_one; + /** reset */ + virtual bool reset(Theory::Effort e) override { return true; } /** register quantifier */ - void registerQuantifier( Node q ); - -//for inst constant -private: + virtual void registerQuantifier(Node q) override; + /** identify */ + virtual std::string identify() const override { return "TermUtil"; } + // for inst constant + private: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; std::map< Node, std::map< Node, unsigned > > d_var_num; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a8930de6e..fdb70c85b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -62,14 +62,15 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; QuantifiersEngine::QuantifiersEngine(context::Context* c, - context::UserContext* u, TheoryEngine* te) + context::UserContext* u, + TheoryEngine* te) : d_te(te), + d_quant_attr(new quantifiers::QuantAttributes(this)), d_conflict_c(c, false), // d_quants(u), d_quants_red(u), d_lemmas_produced_c(u), d_skolemized(u), - d_quant_attr(new quantifiers::QuantAttributes(this)), d_ierCounter_c(c), // d_ierCounter(c), // d_ierCounter_lc(c), @@ -78,16 +79,19 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_presolve_in(u), d_presolve_cache(u), d_presolve_cache_wq(u), - d_presolve_cache_wic(u) { + d_presolve_cache_wic(u) +{ //utilities d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this ); d_util.push_back( d_eq_query ); + // term util must come first + d_term_util = new quantifiers::TermUtil(this); + d_util.push_back(d_term_util); + d_term_db = new quantifiers::TermDb( c, u, this ); d_util.push_back( d_term_db ); - d_term_util = new quantifiers::TermUtil( this ); - if (options::ceGuidedInst()) { d_sygus_tdb = new quantifiers::TermDbSygus(c, this); }else{ @@ -122,6 +126,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if( options::relevantTriggers() ){ d_quant_rel = new QuantRelevance( false ); + d_util.push_back(d_quant_rel); }else{ d_quant_rel = NULL; } @@ -740,16 +745,14 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_quants[f] = false; return false; }else{ - // register with utilities : TODO (#1163) make this a standard call - - d_term_util->registerQuantifier( f ); - d_term_db->registerQuantifier( f ); - d_quant_attr->computeAttributes( f ); - //register with quantifier relevance - if( d_quant_rel ){ - d_quant_rel->registerQuantifier( f ); + // register with utilities + for (unsigned i = 0; i < d_util.size(); i++) + { + d_util[i]->registerQuantifier(f); } - + // compute attributes + d_quant_attr->computeAttributes(f); + for( unsigned i=0; iidentify() << "..." << std::endl; d_modules[i]->preRegisterQuantifier( f ); @@ -765,10 +768,6 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ } //TODO: remove this Node ceBody = d_term_util->getInstConstantBody( f ); - //also register it with the strong solver - //if( options::finiteModelFind() ){ - // ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); - //} Trace("quant-debug") << "...finish." << std::endl; d_quants[f] = true; // flush lemmas @@ -821,9 +820,6 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ void QuantifiersEngine::propagate( Theory::Effort level ){ CodeTimer codeTimer(d_statistics.d_time); - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->propagate( level ); - } } Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index b1608e497..0bb5b10e5 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -124,7 +124,16 @@ private: quantifiers::QModelBuilder* d_builder; /** utility for effectively propositional logic */ QuantEPR * d_qepr; -private: + /** term database */ + quantifiers::TermDb* d_term_db; + /** sygus term database */ + quantifiers::TermDbSygus* d_sygus_tdb; + /** term utilities */ + quantifiers::TermUtil* d_term_util; + /** quantifiers attributes */ + std::unique_ptr d_quant_attr; + + private: /** instantiation engine */ quantifiers::InstantiationEngine* d_inst_engine; /** model engine */ @@ -155,7 +164,8 @@ private: quantifiers::QuantAntiSkolem * d_anti_skolem; /** quantifiers instantiation propagtor */ quantifiers::InstPropagator * d_inst_prop; -public: //effort levels + + public: // effort levels (TODO : make an enum and use everywhere #1293) enum { QEFFORT_CONFLICT, QEFFORT_STANDARD, @@ -194,14 +204,6 @@ private: std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; /** quantifiers that have been skolemized */ BoolMap d_skolemized; - /** term database */ - quantifiers::TermDb* d_term_db; - /** term database */ - quantifiers::TermDbSygus* d_sygus_tdb; - /** term utilities */ - quantifiers::TermUtil* d_term_util; - /** quantifiers attributes */ - std::unique_ptr d_quant_attr; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 1a72944ff..d9e89902c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -523,11 +523,10 @@ public: /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } - /** * Return a decision request, if the theory has one, or the NULL node * otherwise. - * If returning non-null node, hould set priority to + * If returning non-null node, should set priority to * 0 if decision is necessary for model-soundness, * 1 if decision is necessary for completeness, * >1 otherwise. -- 2.30.2