diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-07 09:38:41 -0500 |
| commit | 59b935c1af18ec51efacf87b0e45d9134d3aaa1e (patch) | |
| tree | 57cee5cddf68999e20553ee9746f4a83183e8b99 /src/theory/quantifiers/quant_util.h | |
| parent | 576d50ac7c13233a589771401537b587eb36361e (diff) | |
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
Diffstat (limited to 'src/theory/quantifiers/quant_util.h')
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 2558dcbee..8db79db9c 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -101,6 +101,8 @@ class EqualityQuery { public: EqualityQuery(){} virtual ~EqualityQuery(){}; + /** extends engine */ + virtual bool extendsEngine() { return false; } /** contains term */ virtual bool hasTerm( Node a ) = 0; /** get the representative of the equivalence class of a */ |