diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers/term_database.h | |
parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) |
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
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 376 |
1 files changed, 280 insertions, 96 deletions
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<TNode>& 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<TNode>& 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<TNode>& 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<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, bool, NodeHashFunction> 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<Node>& 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<TNode>& 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<TNode, TNode>& 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<TNode, TNode>& 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<Node> 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 */ |