diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-09 00:51:34 +0200 |
| commit | 433401b05664d9c8827b19455ef7b93fd27efd9d (patch) | |
| tree | 9be15c6804521434d4116b05eb571ecd78ac2767 /src/theory/quantifiers/trigger.h | |
| parent | fc573f3512b5345763755c9d7a061d430c46ae5f (diff) | |
Accept user-provided triggers with variable terms. Flush lemmas before quantifiers check. Minor fix for conjecture generation.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 1a3ae3fcd..74a87591f 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -105,7 +105,6 @@ public: static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false ); public: /** is usable trigger */ - static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); |