summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r--src/theory/quantifiers/term_database.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 13dfa657c..dbd12f8f0 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -316,7 +316,8 @@ public: //general queries concerning quantified formulas wrt modules
static bool isRewriteRule( Node q );
/** get the rewrite rule associated with the quanfied formula */
static Node getRewriteRule( Node q );
-
+ /** is fun def */
+ static bool isFunDef( Node q );
//attributes
private:
std::map< Node, bool > d_qattr_conjecture;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback