diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-27 19:27:57 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-27 19:27:57 -0600 |
| commit | 4698209a407a18ec667a20983328a03d42095e40 (patch) | |
| tree | df0420685321869565d378083bd598b4396fc015 /src/theory/quantifiers/sygus/synth_engine.cpp | |
| parent | a2bba0806dab0e0d4728bbba8e4e6b4160335eeb (diff) | |
Improve cegqi engine trace. (#2714)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 479cfa535..d3eff1750 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -321,7 +321,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) return true; } - Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + Trace("cegqi-engine-debug") + << " *** Check candidate phase..." << std::endl; std::vector<Node> cclems; bool ret = conj->doCheck(cclems); bool addedLemma = false; @@ -343,7 +344,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) } if (addedLemma) { - Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + Trace("cegqi-engine-debug") + << " ...check for counterexample." << std::endl; return true; } else @@ -358,7 +360,8 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) } else { - Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; + Trace("cegqi-engine-debug") + << " *** Refine candidate phase..." << std::endl; std::vector<Node> rlems; conj->doRefine(rlems); bool addedLemma = false; @@ -381,7 +384,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) } if (addedLemma) { - Trace("cegqi-engine") << " ...refine candidate." << std::endl; + Trace("cegqi-engine-debug") << " ...refine candidate." << std::endl; } } return true; |