summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r--src/theory/quantifiers/inst_match.h74
1 files changed, 43 insertions, 31 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index f1c1c952a..ad287c1a3 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file inst_match.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Francois Bobot
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief inst match class
**/
@@ -96,11 +96,12 @@ public:
public:
std::vector< int > d_order;
};/* class InstMatchTrie ImtIndexOrder */
-public:
+
/** the data */
std::map< Node, InstMatchTrie > d_data;
private:
void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
+ void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
public:
InstMatchTrie(){}
~InstMatchTrie(){}
@@ -110,69 +111,80 @@ 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,
- bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+ ImtIndexOrder* imtio = NULL, int index = 0 ) {
+ return !addInstMatch( qe, f, m, modEq, imtio, true, index );
}
bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
- return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+ ImtIndexOrder* imtio = NULL, int index = 0 ) {
+ return !addInstMatch( qe, f, m, modEq, imtio, true, index );
}
/** 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,
- bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
- return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
+ ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
+ return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index );
}
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 );
+ 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 );
}
+ void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+ std::vector< Node > terms;
+ getInstantiations( insts, q, terms, qe );
+ }
void clear() { d_data.clear(); }
};/* class InstMatchTrie */
/** trie for InstMatch objects */
class CDInstMatchTrie {
-public:
+private:
/** the data */
std::map< Node, CDInstMatchTrie* > d_data;
/** is valid */
context::CDO< bool > d_valid;
-private:
+
void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
+ void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const;
public:
CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
- ~CDInstMatchTrie(){}
-public:
+ ~CDInstMatchTrie();
+
/** 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, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0 ) {
- return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+ bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
+ int index = 0 ) {
+ return !addInstMatch( qe, q, m, c, modEq, index, true );
}
- bool existsInstMatch( QuantifiersEngine* qe, Node f, 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 );
+ bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
+ int index = 0 ) {
+ return !addInstMatch( qe, q, m, c, modEq, 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 modInst = false, int index = 0, bool onlyExist = false ) {
- return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
+ bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
+ int index = 0, bool onlyExist = false ) {
+ return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist );
}
- bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
- bool modInst = false, int index = 0, bool onlyExist = false );
+ bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = 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 );
}
+ void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) {
+ std::vector< Node > terms;
+ getInstantiations( insts, q, terms, qe );
+ }
};/* class CDInstMatchTrie */
@@ -190,10 +202,10 @@ public:
public:
/** add match m, return true if successful */
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 );
+ return d_imt.addInstMatch( qe, f, m, modEq, 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 );
+ return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio );
}
};/* class InstMatchTrieOrdered */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback