diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 17:10:47 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 17:10:47 +0000 |
commit | bbcfb5208c6c0f343d1a63b129c54914f66b2701 (patch) | |
tree | f2369b3cc07121645ef0c8c3a415f243f5a4fcb9 /src/theory/quantifiers/inst_match.h | |
parent | 5b8b6acd9091e2afec654ebed1332d6755bbb7d9 (diff) |
first draft of new inst gen method (still with bugs), some cleanup of quantifiers code
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 52 |
1 files changed, 34 insertions, 18 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 90a24322a..feab91837 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -114,20 +114,39 @@ public: bool merge( EqualityQuery* q, InstMatch& m ); /** debug print method */ void debugPrint( const char* c ); + /** is complete? */ + bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } /** make complete */ void makeComplete( Node f, QuantifiersEngine* qe ); /** make internal: ensure that no term in d_map contains instantiation constants */ void makeInternal( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); - /** apply rewrite */ - void applyRewrite(); /** compute d_match */ - void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ); + //void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ); /** compute d_match */ - void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ); + //void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ); + /** get value */ + Node getValue( Node var ); /** clear */ void clear(){ d_map.clear(); } + /** is_empty */ + bool empty(){ return d_map.empty(); } + /** to stream */ + inline void toStream(std::ostream& out) const { + out << "INST_MATCH( "; + for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){ + if( it != d_map.begin() ){ out << ", "; } + out << it->first << " -> " << it->second; + } + out << " )"; + } + + + //for rewrite rules + + /** apply rewrite */ + void applyRewrite(); /** erase */ template<class Iterator> void erase(Iterator begin, Iterator end){ @@ -136,8 +155,8 @@ public: }; } void erase(Node node){ d_map.erase(node); } - /** is_empty */ - bool empty(){ return d_map.empty(); } + /** get */ + Node get( TNode var ) { return d_map[var]; } /** set */ void set(TNode var, TNode n){ //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ; @@ -146,7 +165,6 @@ public: var.getType() == n.getType() ); d_map[var] = n; } - Node get(TNode var){ return d_map[var]; } size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; @@ -155,15 +173,6 @@ public: /* Node used for matching the trigger only for mono-trigger (just for efficiency because I need only that) */ Node d_matched; - /** to stream */ - inline void toStream(std::ostream& out) const { - out << "INST_MATCH( "; - for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it != d_map.begin() ){ out << ", "; } - out << it->first << " -> " << it->second; - } - out << " )"; - } };/* class InstMatch */ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { @@ -182,7 +191,7 @@ private: /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ); /** exists match */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio ); + bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ); public: /** the data */ std::map< Node, InstMatchTrie > d_data; @@ -190,11 +199,18 @@ public: InstMatchTrie(){} ~InstMatchTrie(){} public: + /** return true if m exists in this trie + modEq is if we check modulo equality + modInst is if we return true if m is an instance of a match that exists + */ + bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, + ImtIndexOrder* imtio = NULL, bool modInst = false ); /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, ImtIndexOrder* imtio = NULL ); + bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, + ImtIndexOrder* imtio = NULL, bool modInst = false ); };/* class InstMatchTrie */ class InstMatchTrieOrdered { |