From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Jul 2021 15:44:01 +0000 (-0500)
Subject: Standard output for trigger selection (#6841)
X-Git-Tag: cvc5-1.0.0~1520
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0824de45d26f02a6422e596a3b743e9ea455bd2;p=cvc5.git

Standard output for trigger selection (#6841)

Fixes #6259.
---

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]))