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.h | |
parent | 9854e505aeae1ac86ea75e98131dd8643349df60 (diff) |
Make getSynthSolution return a Bool (#3306)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.h')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index e099657ad..b5880b0c1 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -60,8 +60,15 @@ class SynthEngine : public QuantifiersModule public: SynthEngine(QuantifiersEngine* qe, context::Context* c); ~SynthEngine(); - + /** presolve + * + * Called at the beginning of each call to solve a synthesis problem, which + * may be e.g. a check-synth or get-abduct call. + */ + void presolve() override; + /** needs check, return true if e is last call */ bool needsCheck(Theory::Effort e) override; + /** always needs model at effort QEFFORT_MODEL */ QEffort needsModel(Theory::Effort e) override; /* Call during quantifier engine's check */ void check(Theory::Effort e, QEffort quant_e) override; @@ -81,7 +88,7 @@ class SynthEngine : public QuantifiersModule * For details on what is added to sol_map, see * SynthConjecture::getSynthSolutions. */ - void getSynthSolutions(std::map<Node, Node>& sol_map); + bool getSynthSolutions(std::map<Node, Node>& sol_map); /** preregister assertion (before rewrite) * * The purpose of this method is to inform the solution reconstruction |