diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:33 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:41 -0500 |
commit | 5e4ed407978b892e04de00994be535f58fb33257 (patch) | |
tree | 5ff2dfbf18845113c5ea0fa43e8792532498d2ec /src/theory/quantifiers/inst_match.h | |
parent | c833e176a81eb193462c0efde0c6c2f28c5159fb (diff) |
More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index fbdef61c2..a87d2704e 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -128,6 +128,7 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); @@ -157,24 +158,25 @@ public: 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, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } - bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } /** 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, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ) { - return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist ); + return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist ); } - bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); |