diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-07-31 12:49:28 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-07-31 12:49:28 +0200 |
commit | a9f4d3e2aed0c6d8d8b218c5f5d2bc95af2d45a6 (patch) | |
tree | f05ce319e03a0c29cf4b220855f24884012ad954 /src/theory/quantifiers/modes.h | |
parent | c4d8629dc65d283a2fe03f6ad46ff3a65b9b62e4 (diff) |
New module for generating candidate equality conjectures used in inductive proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).
Diffstat (limited to 'src/theory/quantifiers/modes.h')
-rw-r--r-- | src/theory/quantifiers/modes.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 112e052c2..26978c8f9 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -107,6 +107,15 @@ typedef enum { USER_PAT_MODE_IGNORE, } UserPatMode; +typedef enum { + /** default for trigger selection */ + TRIGGER_SEL_DEFAULT, + /** only consider minimal terms for triggers */ + TRIGGER_SEL_MIN, + /** only consider maximal terms for triggers */ + TRIGGER_SEL_MAX, +} TriggerSelMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ |