diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 10 |
2 files changed, 11 insertions, 11 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{ 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 */ |