Standard output for trigger selection (#6841)

Fixes #6259.

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 315a38f10df5928a52215c7ebba88e6afa8104c4..2223664d16ba32fecc242976c7c9bdfb86488606 100644 (file)
--- 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 8c4d593227da1dd292a379e6792ebfcc4d6dc5de..ab237fc6cd0e5fdcfd2d2836eaef8754c2821a36 100644 (file)
--- 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 3a78819ea0d7565603952b8f18add55477ef739e..62558e2c65c916edc859a72bcd53b40be01d656d 100644 (file)
--- 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]))