diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
| commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
| tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/theory/quantifiers/inst_match.h | |
| parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) | |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 2cf63210b..accd3baed 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,7 +101,7 @@ public: /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -128,9 +128,9 @@ 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( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class InstMatchTrie */ @@ -142,7 +142,7 @@ public: /** is valid */ context::CDO< bool > d_valid; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -169,9 +169,9 @@ 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( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class CDInstMatchTrie */ |