diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:02:51 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:03:20 -0500 |
| commit | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (patch) | |
| tree | ebe6334ca8a415a4d5a24a83ee40441419c93876 /src/theory/quantifiers/trigger.h | |
| parent | ae1d4e4f05fdc2db61d7de7efee5bd567363ceef (diff) | |
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/trigger.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 234025e7b..8d8f01926 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -137,9 +137,9 @@ private: static Node getIsUsableEq( Node q, Node eq ); static bool isUsableEqTerms( Node q, Node n1, Node n2 ); /** collect all APPLY_UF pattern terms for f in n */ - static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, + static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, - bool pol, bool hasPol, bool epol, bool hasEPol ); + bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false ); std::vector< Node > d_nodes; |