diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-14 14:46:53 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-14 14:47:09 -0500 |
| commit | 478b935ba5e2b9eda4eb21f7651747c5325229b1 (patch) | |
| tree | 6492b5a4598efadf533859c9d45bafce9295a899 /src/theory/quantifiers/inst_match.h | |
| parent | e0a291555fc4710c39a75eac19039a063c166cea (diff) | |
Finish --dump-instantiations option. Update scripts.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index accd3baed..d728d18a2 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -41,7 +41,7 @@ public: std::vector< Node > d_vals; public: InstMatch(){} - InstMatch( Node f ); + explicit InstMatch( TNode f ); InstMatch( InstMatch* m ); /** fill all unfilled values with m */ @@ -101,7 +101,7 @@ public: /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -129,7 +129,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 ); void print( std::ostream& out, Node q ) const{ - std::vector< Node > terms; + std::vector< TNode > terms; print( out, q, terms ); } };/* class InstMatchTrie */ @@ -142,7 +142,7 @@ public: /** is valid */ context::CDO< bool > d_valid; private: - void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -170,7 +170,7 @@ public: 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 ); void print( std::ostream& out, Node q ) const{ - std::vector< Node > terms; + std::vector< TNode > terms; print( out, q, terms ); } };/* class CDInstMatchTrie */ |