diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-07 10:44:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-07 15:44:01 +0000 |
| commit | e0824de45d26f02a6422e596a3b743e9ea455bd2 (patch) | |
| tree | f4be53cb4deee0613270e5ecd38409ef83ec9b39 /src/theory/quantifiers | |
| parent | 468ba87a10e3f3fadf7c48a0b3923ecc489616ad (diff) | |
Standard output for trigger selection (#6841)
Fixes #6259.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 15 |
2 files changed, 19 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8c4d59322..ab237fc6c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" +#include "options/base_options.h" +#include "options/outputc.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/ematching/trigger_database.h" #include "theory/quantifiers/quant_relevance.h" @@ -145,6 +147,8 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, && d_auto_gen_trigger[1][f].empty() && f.getNumChildren() == 2) { Trace("trigger-warn") << "Could not find trigger for " << f << std::endl; + Output(options::OutputTag::TRIGGER) + << "(no-trigger " << f << ")" << std::endl; } } if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL) diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3a78819ea..62558e2c6 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/ematching/trigger.h" #include "expr/skolem_manager.h" +#include "options/base_options.h" +#include "options/outputc.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/inst_match_generator.h" @@ -67,6 +69,19 @@ Trigger::Trigger(QuantifiersState& qs, Trace("trigger") << " " << n << std::endl; } } + if (Output.isOn(options::OutputTag::TRIGGER)) + { + QuantAttributes& qa = d_qreg.getQuantAttributes(); + Output(options::OutputTag::TRIGGER) + << "(trigger " << qa.quantToString(q) << " ("; + for (size_t i = 0, nnodes = d_nodes.size(); i < nnodes; i++) + { + // note we must display the original form, so we go back to bound vars + Node ns = d_qreg.substituteInstConstantsToBoundVariables(d_nodes[i], q); + Output(options::OutputTag::TRIGGER) << (i > 0 ? " " : "") << ns; + } + Output(options::OutputTag::TRIGGER) << "))" << std::endl; + } QuantifiersStatistics& stats = qs.getStats(); if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) |