syqi: Add debug information for dumping instantiations. (#6978)

Adds the datatype values as debug information for dumping instantiations produced by --sygus-inst.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 286d5f42be851858253a71e4ea5a48e982bad86d..21852f25a21ad7f919e008a9bdb071bbcf85d63b 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -258,7 +258,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
     Assert(inst_constants.size() == dt_evals.size());
     Assert(inst_constants.size() == q[0].getNumChildren());
 
-    std::vector<Node> terms, eval_unfold_lemmas;
+    std::vector<Node> terms, values, eval_unfold_lemmas;
     for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
     {
       Node dt_var = inst_constants[i];
@@ -266,6 +266,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
       Node value = model->getValue(dt_var);
       Node t = datatypes::utils::sygusToBuiltin(value);
       terms.push_back(t);
+      values.push_back(value);
 
       std::vector<Node> exp;
       syexplain.getExplanationForEquality(dt_var, value, exp);
@@ -285,7 +286,10 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
 
     if (mode == options::SygusInstMode::PRIORITY_INST)
     {
-      if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI))
+      if (!inst->addInstantiation(q,
+                                  terms,
+                                  InferenceId::QUANTIFIERS_INST_SYQI,
+                                  nm->mkNode(kind::SEXPR, values)))
       {
         sendEvalUnfoldLemmas(eval_unfold_lemmas);
       }
@@ -294,13 +298,19 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
     {
       if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
       {
-        inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
+        inst->addInstantiation(q,
+                               terms,
+                               InferenceId::QUANTIFIERS_INST_SYQI,
+                               nm->mkNode(kind::SEXPR, values));
       }
     }
     else
     {
       Assert(mode == options::SygusInstMode::INTERLEAVE);
-      inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI);
+      inst->addInstantiation(q,
+                             terms,
+                             InferenceId::QUANTIFIERS_INST_SYQI,
+                             nm->mkNode(kind::SEXPR, values));
       sendEvalUnfoldLemmas(eval_unfold_lemmas);
     }
   }