From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 24 Oct 2018 20:20:18 +0000 (-0500)
Subject: Minor improvement to sygus trace (#2675)
X-Git-Tag: cvc5-1.0.0~4386
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1955e4b504e95ed64bc7dcc6b1329eb5b796f565;p=cvc5.git

Minor improvement to sygus trace (#2675)
---

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 06f041d93..79bec60ee 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -562,7 +562,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
   Assert(vals.size() == candidates.size());
   Node sbody = d_base_body.substitute(
       candidates.begin(), candidates.end(), vals.begin(), vals.end());
-  Trace("cegis-sample-debug") << "Sample " << sbody << std::endl;
+  Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl;
   // do eager unfolding
   std::map<Node, Node> visited_n;
   sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index adc20008e..b95af719e 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -458,11 +458,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   Node lem;
   // introduce the skolem variables
   std::vector<Node> sks;
+  std::vector<Node> vars;
   if (constructed_cand)
   {
     if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
     {
-      std::vector<Node> vars;
       for (const Node& v : inst[0][0])
       {
         Node sk = nm->mkSkolem("rsk", v.getType());
@@ -527,10 +527,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       {
         Trace("cegqi-engine") << "  * Verification lemma failed for:\n   ";
         // do not send out
-        for (const Node& v : d_ce_sk_vars)
+        for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
         {
+          Node v = d_ce_sk_vars[i];
           Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr()));
-          Trace("cegqi-engine") << v << " -> " << mv << " ";
+          Trace("cegqi-engine") << vars[i] << " -> " << mv << " ";
           d_ce_sk_var_mvs.push_back(mv);
         }
         Trace("cegqi-engine") << std::endl;