diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-17 17:35:56 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-17 17:35:56 -0600 |
| commit | b0d7ac44fb7be5c56cd0c743114e792a985bb3b7 (patch) | |
| tree | 4d5e8de3b66de4af0fe225d594edd78726b8bb1d /src/theory/quantifiers/inst_match.h | |
| parent | c603a047ac534ed4caafb128b5d333e05e1fd191 (diff) | |
Refactor quantifiers attributes. Make quantifier elimination robust to preprocessing, implement get-qe-disjunct.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 24 |
1 files changed, 8 insertions, 16 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index abe31b48d..35353863c 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,7 +101,7 @@ public: 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< TNode >& vars, std::vector< TNode >& terms ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -132,13 +132,9 @@ public: std::vector< TNode > terms; print( out, q, terms ); } - void getInstantiations( std::vector< Node >& insts, Node q ) { - std::vector< TNode > terms; - std::vector< TNode > vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars.push_back( q[0][i] ); - } - getInstantiations( insts, q, vars, 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 */ @@ -152,7 +148,7 @@ public: 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< TNode >& vars, 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(){} @@ -183,13 +179,9 @@ public: std::vector< TNode > terms; print( out, q, terms ); } - void getInstantiations( std::vector< Node >& insts, Node q ) { - std::vector< TNode > terms; - std::vector< TNode > vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - vars.push_back( q[0][i] ); - } - getInstantiations( insts, q, vars, terms ); + void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) { + std::vector< Node > terms; + getInstantiations( insts, q, terms, qe ); } };/* class CDInstMatchTrie */ |