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.cpp | |
| parent | e0a291555fc4710c39a75eac19039a063c166cea (diff) | |
Finish --dump-instantiations option. Update scripts.
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
| -rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 703a44d03..292190168 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -27,7 +27,7 @@ namespace CVC4 { namespace theory { namespace inst { -InstMatch::InstMatch( Node f ) { +InstMatch::InstMatch( TNode f ) { for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ d_vals.push_back( Node::null() ); } @@ -198,12 +198,12 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } -void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const { +void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) out << ", "; - //out << terms[i]; + if( i>0 ){ out << ", ";} + out << terms[i]; } out << " )" << std::endl; }else{ @@ -282,13 +282,13 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } -void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{ +void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ if( i>0 ) out << ", "; - //out << terms[i]; + out << terms[i]; } out << " )" << std::endl; }else{ |