User-facing print debug option for sygus candidates (#4720)

This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:

(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 227f43c46b9edbb6337d03997e0a3022757f18f8..2b47570eda230371bd8b7481fde7775d6e038d4e 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1608,6 +1608,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
 
+[[option]]
+  name       = "debugSygus"
+  category   = "regular"
+  long       = "debug-sygus"
+  type       = "bool"
+  default    = "false"
+  help       = "print enumerated terms and candidates generated by the sygus solver (for debugging)"
+
 # CEGQI applied to general quantified formulas
 
 [[option]]

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index a28e76d902bcd1586841b60f38365ce0eb71611c..6ade49b6d3d6723278f8767ad5a9d8bd70466ab1 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -387,6 +387,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     }
   }
 
+  bool printDebug = options::debugSygus();
   if (!constructed_cand)
   {
     // get the model value of the relevant terms from the master module
@@ -420,10 +421,13 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
       return !activeIncomplete;
     }
-    // debug print
-    if (Trace.isOn("sygus-engine"))
+    // Must separately compute whether trace is on due to compilation of
+    // Trace.isOn.
+    bool traceIsOn = Trace.isOn("sygus-engine");
+    if (printDebug || traceIsOn)
     {
       Trace("sygus-engine") << "  * Value is : ";
+      std::stringstream sygusEnumOut;
       for (unsigned i = 0, size = terms.size(); i < size; i++)
       {
         Node nv = enum_values[i];
@@ -431,6 +435,10 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         TypeNode tn = onv.getType();
         std::stringstream ss;
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+        if (printDebug)
+        {
+          sygusEnumOut << " " << ss.str();
+        }
         Trace("sygus-engine") << terms[i] << " -> ";
         if (nv.isNull())
         {
@@ -448,6 +456,12 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         }
       }
       Trace("sygus-engine") << std::endl;
+      if (printDebug)
+      {
+        Options& sopts = smt::currentSmtEngine()->getOptions();
+        std::ostream& out = *sopts.getOut();
+        out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
+      }
     }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(
@@ -535,6 +549,21 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> vars;
   if (constructed_cand)
   {
+    if (printDebug)
+    {
+      Options& sopts = smt::currentSmtEngine()->getOptions();
+      std::ostream& out = *sopts.getOut();
+      out << "(sygus-candidate ";
+      Assert(d_quant[0].getNumChildren() == candidate_values.size());
+      for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
+      {
+        Node v = candidate_values[i];
+        std::stringstream ss;
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, v);
+        out << "(" << d_quant[0][i] << " " << ss.str() << ")";
+      }
+      out << ")" << std::endl;
+    }
     if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
     {
       for (const Node& v : inst[0][0])

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0449107af4f842389ab59be1c7d57f18aaa27744..18bf6d104eba66ecab2174281cb03a630d4d3187 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1045,6 +1045,7 @@ set(regress_0_tests
   regress0/sygus/parse-bv-let.sy
   regress0/sygus/pbe-pred-contra.sy
   regress0/sygus/pLTL-sygus-syntax-err.sy
+  regress0/sygus/print-debug.sy
   regress0/sygus/print-define-fun.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/sygus-no-wf.sy

diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy
new file mode 100644 (file)
index 0000000..0de4312
--- /dev/null
+++ b/test/regress/regress0/sygus/print-debug.sy
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --debug-sygus
+; EXPECT: (sygus-enum 0)
+; EXPECT: (sygus-candidate (f 0))
+; EXPECT: (sygus-enum 1)
+; EXPECT: (sygus-candidate (f 1))
+; EXPECT: unsat
+; EXPECT: (define-fun f () Int 1)
+(set-logic LIA)
+
+(synth-fun f () Int ((Start Int)) ((Start Int (0 1))))
+
+(constraint (not (= f 0)))
+
+(check-synth)