diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-22 11:01:05 +0200 |
commit | a7a9ba359a2a8a26f20ac8fdf5292c4e0e27c76a (patch) | |
tree | a62e3c29bb702a2e890b234504bbc121c4da2619 /src/theory/quantifiers/trigger.h | |
parent | 7e133dbb7c1adf077102d377d1f7eecae1640ee1 (diff) |
Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
-rw-r--r-- | src/theory/quantifiers/trigger.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index f601a02ab..bd4c19dba 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -108,6 +108,7 @@ public: static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); + static bool isCbqiKind( Kind k ); static bool isSimpleTrigger( Node n ); static bool isBooleanTermTrigger( Node n ); static bool isPureTheoryTrigger( Node n ); |