summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r--src/theory/quantifiers/inst_match.h3
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(); };
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback