diff options
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 127f83c60..72447fd66 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -92,8 +92,11 @@ public: void erase(Node node){ d_map.erase(node); } /** get */ Node get( TNode var ) { return d_map[var]; } + Node get( QuantifiersEngine* qe, Node f, int i ); /** set */ void set(TNode var, TNode n); + void set( QuantifiersEngine* qe, Node f, int i, TNode n ); + /** size */ size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; |