diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-18 17:34:00 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-18 17:34:00 +0000 |
commit | a441252481616ff4851f208caffce826a026ae30 (patch) | |
tree | 67df7986753dfbea35cd0a5a3264e7be1378a1d2 /src/theory/quantifiers/inst_match.h | |
parent | 39020386be1c6cb304a5bfd1eaca37af46bb0bfc (diff) |
support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 41ebb63d2..c8f843c90 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -92,14 +92,7 @@ public: /** get */ Node get( TNode var ) { return d_map[var]; } /** set */ - void set(TNode var, TNode n){ - //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ; - Assert( !var.isNull() ); - Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - //var.getType() == n.getType() - n.getType().isSubtypeOf( var.getType() ) ); - d_map[var] = n; - } + void set(TNode var, TNode n); size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; |