diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 17:23:22 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-28 17:23:22 +0100 |
| commit | db982d9329981683c8d791aadba7e97fa98b0bd3 (patch) | |
| tree | 09e4d6a472789322a43b5443f2276d38e11a956b /src/theory/quantifiers/term_database.h | |
| parent | 55323fd7283d758caf31e637be237d2416b86167 (diff) | |
Preprocessing step for finding finite runs of well-defined function definitions using FMF.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 3 |
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; |