From e0824de45d26f02a6422e596a3b743e9ea455bd2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Jul 2021 10:44:01 -0500 Subject: [PATCH] Standard output for trigger selection (#6841) Fixes #6259. --- src/options/base_options.toml | 3 +++ .../ematching/inst_strategy_e_matching.cpp | 4 ++++ src/theory/quantifiers/ematching/trigger.cpp | 15 +++++++++++++++ 3 files changed, 22 insertions(+) diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 315a38f10..2223664d1 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -219,6 +219,9 @@ public = true [[option.mode.SYGUS]] name = "sygus" help = "print enumerated terms and candidates generated by the sygus solver" +[[option.mode.TRIGGER]] + name = "trigger" + help = "print selected triggers for quantified formulas" # Stores then enabled output tags. [[option]] 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])) -- 2.30.2