diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 16:12:29 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 16:12:29 -0500 |
commit | a34f29798b3f4d1f83e1ced57fe53db53b9956f0 (patch) | |
tree | e04a6211d7e1968688da3fa48014cec861434d74 /src/theory/quantifiers | |
parent | 4b86268a71d0d6fd179134889f7d15304623b130 (diff) |
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.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 33 |
1 files changed, 31 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index a28e76d90..6ade49b6d 100644 --- 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]) |