From 9a2913c2f1a22ed43ed772467ec42ba2262bee17 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Nov 2019 12:23:34 -0600 Subject: Make getSynthSolution return a Bool (#3306) --- src/theory/quantifiers/sygus/synth_engine.cpp | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp') diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d13bd2dcf..73105af6f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -41,6 +41,17 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) } SynthEngine::~SynthEngine() {} + +void SynthEngine::presolve() +{ + Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl; + for (unsigned i = 0, size = d_conjs.size(); i < size; i++) + { + d_conjs[i]->presolve(); + } + Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl; +} + bool SynthEngine::needsCheck(Theory::Effort e) { return e >= Theory::EFFORT_LAST_CALL; @@ -130,7 +141,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) void SynthEngine::assignConjecture(Node q) { - Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; + Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl; if (options::sygusQePreproc()) { // the following does quantifier elimination as a preprocess step @@ -376,15 +387,22 @@ void SynthEngine::printSynthSolution(std::ostream& out) } } -void SynthEngine::getSynthSolutions(std::map& sol_map) +bool SynthEngine::getSynthSolutions(std::map& sol_map) { + bool ret = true; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { if (d_conjs[i]->isAssigned()) { - d_conjs[i]->getSynthSolutions(sol_map); + if (!d_conjs[i]->getSynthSolutions(sol_map)) + { + // if one conjecture fails, we fail overall + ret = false; + break; + } } } + return ret; } void SynthEngine::preregisterAssertion(Node n) -- cgit v1.2.3