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/macros.cpp | |
| 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/macros.cpp')
| -rw-r--r-- | src/theory/quantifiers/macros.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 90d01ac28..582599680 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -153,7 +153,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { d_qe->getTermDatabase()->getVarContainsNode( f, icn, var ); Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; std::vector< Node > trigger_var; - inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var ); + inst::Trigger::getTriggerVariables( icn, f, trigger_var ); Trace("macros-debug2") << "Done." << std::endl; //only if all variables are also trigger variables return trigger_var.size()>=var.size(); |