diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
commit | d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7 (patch) | |
tree | f730bb17eba9412258c47617f144510d722d6006 /src/theory/quantifiers/inst_match.h | |
parent | bbcfb5208c6c0f343d1a63b129c54914f66b2701 (diff) |
more cleanup of quantifiers code
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index feab91837..a0db1336f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -122,10 +122,6 @@ public: void makeInternal( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); - /** compute d_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 ); /** get value */ Node getValue( Node var ); /** clear */ @@ -191,7 +187,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 existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ); + bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); public: /** the data */ std::map< Node, InstMatchTrie > d_data; @@ -204,16 +200,16 @@ public: 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 ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); /** 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 modInst = false ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); };/* class InstMatchTrie */ -class InstMatchTrieOrdered { +class InstMatchTrieOrdered{ private: InstMatchTrie::ImtIndexOrder* d_imtio; InstMatchTrie d_imt; @@ -226,8 +222,11 @@ public: InstMatchTrie* getTrie() { return &d_imt; } public: /** add match m, return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, d_imtio ); + bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio ); + } + bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio ); } };/* class InstMatchTrieOrdered */ |