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.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8753c0bb1..21220491f 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -78,6 +78,7 @@ public:
void applyRewrite();
/** get */
Node get( int i );
+ void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst );
/** set */
void setValue( int i, TNode n );
bool set( QuantifiersEngine* qe, int i, TNode n );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback