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