diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-23 23:40:29 +0000 |
commit | 304404e3709ff7e95156c87f65a3e2647d9f3441 (patch) | |
tree | 10fd1c4cc42567c3fac5fd91ad76aef3d49975b5 /src/theory/quantifiers/inst_match.h | |
parent | 697dd317af39a896865c99b922e80baac2bb4b23 (diff) |
more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 233 |
1 files changed, 2 insertions, 231 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index a0db1336f..426adc02d 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -20,81 +20,19 @@ #include "util/hash.h" #include <ext/hash_set> -#include <iostream> #include <map> #include "context/cdlist.h" -#include "theory/quantifiers/candidate_generator.h" - -//#define USE_EFFICIENT_E_MATCHING +#include "expr/node.h" namespace CVC4 { namespace theory { -/** Attribute true for nodes that should not be used for matching */ -struct NoMatchAttributeId {}; -/** use the special for boolean flag */ -typedef expr::Attribute< NoMatchAttributeId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > NoMatchAttribute; - -// attribute for "contains instantiation constants from" -struct InstConstantAttributeId {}; -typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; - -struct InstLevelAttributeId {}; -typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; - -struct InstVarNumAttributeId {}; -typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; - -// Attribute that tell if a node have been asserted in this branch -struct AvailableInTermDbId {}; -/** use the special for boolean flag */ -typedef expr::Attribute<AvailableInTermDbId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > AvailableInTermDb; - - class QuantifiersEngine; -namespace quantifiers{ - class TermArgTrie; -} - -namespace uf{ - class InstantiatorTheoryUf; - class TheoryUF; -}/* CVC4::theory::uf namespace */ +class EqualityQuery; namespace inst { -class EqualityQuery { -public: - EqualityQuery(){} - virtual ~EqualityQuery(){}; - /** contains term */ - virtual bool hasTerm( Node a ) = 0; - /** get the representative of the equivalence class of a */ - virtual Node getRepresentative( Node a ) = 0; - /** returns true if a and b are equal in the current context */ - virtual bool areEqual( Node a, Node b ) = 0; - /** returns true is a and b are disequal in the current context */ - virtual bool areDisequal( Node a, Node b ) = 0; - /** 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. - */ - virtual Node getInternalRepresentative( Node a ) = 0; - /** get the equality engine associated with this query */ - virtual eq::EqualityEngine* getEngine() = 0; - /** get the equivalence class of a */ - virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; -};/* class EqualityQuery */ - /** basic class defining an instantiation */ class InstMatch { /* map from variable to ground terms */ @@ -230,176 +168,9 @@ public: } };/* class InstMatchTrieOrdered */ -/** base class for producing InstMatch objects */ -class IMGenerator { -public: - /** reset instantiation round (call this at beginning of instantiation round) */ - virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0; - /** get the next match. must call reset( eqc ) before this function. */ - virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0; - /** add instantiations directly */ - virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0; - /** add ground term t, called when t is added to term db */ - virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0; -};/* class IMGenerator */ - - -class InstMatchGenerator : public IMGenerator { -private: - /** candidate generator */ - CandidateGenerator* d_cg; - /** policy to use for matching */ - int d_matchPolicy; - /** children generators */ - std::vector< InstMatchGenerator* > d_children; - std::vector< int > d_children_index; - /** partial vector */ - std::vector< InstMatch > d_partial; - /** eq class */ - Node d_eq_class; - /** for arithmetic matching */ - std::map< Node, Node > d_arith_coeffs; - /** initialize pattern */ - void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ); - void initializePattern( Node pat, QuantifiersEngine* qe ); -public: - enum { - //options for producing matches - MATCH_GEN_DEFAULT = 0, - MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E-matching for SMT solvers - //others (internally used) - MATCH_GEN_INTERNAL_ARITHMETIC, - MATCH_GEN_INTERNAL_ERROR, - }; -private: - /** get the next match. must call d_cg->reset( ... ) before using. - only valid for use where !d_match_pattern.isNull(). - */ - bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false ); - /** for arithmetic */ - bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ); -public: - /** get the match against ground term or formula t. - d_match_pattern and t should have the same shape. - only valid for use where !d_match_pattern.isNull(). - */ - bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ); - - /** constructors */ - InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 ); - InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); - /** destructor */ - ~InstMatchGenerator(){} - /** The pattern we are producing matches for. - If null, this is a multi trigger that is merging matches from d_children. - */ - Node d_pattern; - /** match pattern */ - Node d_match_pattern; -public: - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ); - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ); - /** get the next match. must call reset( eqc ) before this function. */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector<Node> & vars); - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGenerator */ - -/** smart multi-trigger implementation */ -class InstMatchGeneratorMulti : public IMGenerator { -private: - /** indexed trie */ - typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie; - /** process new match */ - void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ); - /** process new instantiations */ - void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr, - std::vector< IndexedTrie >& unique_var_tries, - int trieIndex, int childIndex, int endChildIndex, bool modEq ); - /** process new instantiations 2 */ - void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, - std::vector< IndexedTrie >& unique_var_tries, - int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 ); -private: - /** var contains (variable indices) for each pattern node */ - std::map< Node, std::vector< int > > d_var_contains; - /** variable indices contained to pattern nodes */ - std::map< int, std::vector< Node > > d_var_to_node; - /** quantifier to use */ - Node d_f; - /** policy to use for matching */ - int d_matchPolicy; - /** children generators */ - std::vector< InstMatchGenerator* > d_children; - /** inst match tries for each child */ - std::vector< InstMatchTrieOrdered > d_children_trie; - /** calculate matches */ - void calculateMatches( QuantifiersEngine* qe ); -public: - /** constructors */ - InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 ); - /** destructor */ - ~InstMatchGeneratorMulti(){} - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ); - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ); - /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; } - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGeneratorMulti */ - -/** smart (single)-trigger implementation */ -class InstMatchGeneratorSimple : public IMGenerator { -private: - /** quantifier for match term */ - Node d_f; - /** match term */ - Node d_match_pattern; - /** add instantiations */ - void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ); -public: - /** constructors */ - InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){} - /** destructor */ - ~InstMatchGeneratorSimple(){} - /** reset instantiation round (call this whenever equivalence classes have changed) */ - void resetInstantiationRound( QuantifiersEngine* qe ) {} - /** reset, eqc is the equivalence class to search in (any if eqc=null) */ - void reset( Node eqc, QuantifiersEngine* qe ) {} - /** get the next match. must call reset( eqc ) before this function. (not implemented) */ - bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; } - /** return true if whatever Node is substituted for the variables the - given Node can't match the pattern */ - bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; } - /** add instantiations */ - int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ); - /** add ground term t, possibly add instantiations */ - int addTerm( Node f, Node t, QuantifiersEngine* qe ); -};/* class InstMatchGeneratorSimple */ - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; -typedef CVC4::theory::inst::EqualityQuery EqualityQuery; }/* CVC4::theory namespace */ }/* CVC4 namespace */ |