diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-04 12:23:34 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-04 12:23:34 -0600 |
commit | 9a2913c2f1a22ed43ed772467ec42ba2262bee17 (patch) | |
tree | d8465f1a1deefc91397d2f426630c92b7a797133 /src/theory/quantifiers/sygus/synth_engine.cpp | |
parent | 9854e505aeae1ac86ea75e98131dd8643349df60 (diff) |
Make getSynthSolution return a Bool (#3306)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 24 |
1 files changed, 21 insertions, 3 deletions
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<Node, Node>& sol_map) +bool SynthEngine::getSynthSolutions(std::map<Node, Node>& 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) |