From: Andrew Reynolds Date: Fri, 23 Aug 2019 14:31:21 +0000 (-0500) Subject: Pass synthesis conjecture to sygus modules (#3212) X-Git-Tag: cvc5-1.0.0~4001 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=847f415d9bd9aa98470109fbdc37fd379a79cb4e;p=cvc5.git Pass synthesis conjecture to sygus modules (#3212) --- diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 301d772bf..1e8012697 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,7 +39,8 @@ Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) } } -bool Cegis::initialize(Node n, +bool Cegis::initialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) { @@ -61,10 +62,11 @@ bool Cegis::initialize(Node n, TypeNode bt = d_base_body.getType(); d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples()); } - return processInitialize(n, candidates, lemmas); + return processInitialize(conj, n, candidates, lemmas); } -bool Cegis::processInitialize(Node n, +bool Cegis::processInitialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) { diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index a295f6a40..891379992 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -44,7 +44,8 @@ class Cegis : public SygusModule Cegis(QuantifiersEngine* qe, SynthConjecture* p); ~Cegis() override {} /** initialize */ - virtual bool initialize(Node n, + virtual bool initialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) override; /** get term list */ @@ -77,14 +78,21 @@ class Cegis : public SygusModule */ Node d_base_body; //----------------------------------cegis-implementation-specific - /** do cegis-implementation-specific initialization for this class */ - virtual bool processInitialize(Node n, + /** + * Do cegis-implementation-specific initialization for this class. The return + * value and behavior of this function is the same as initialize(...) above. + */ + virtual bool processInitialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas); /** do cegis-implementation-specific post-processing for construct candidate * * satisfiedRl is whether all refinement lemmas are satisfied under the * substitution { enums -> enum_values }. + * + * The return value and behavior of this function is the same as + * constructCandidates(...) above. */ virtual bool processConstructCandidates(const std::vector& enums, const std::vector& enum_values, diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 6e9467b7c..399a9576c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -35,7 +35,8 @@ CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p) } CegisUnif::~CegisUnif() {} -bool CegisUnif::processInitialize(Node n, +bool CegisUnif::processInitialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) { diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index a2e7be1c1..ac859750f 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -233,7 +233,8 @@ class CegisUnif : public Cegis private: /** do cegis-implementation-specific initialization for this class */ - bool processInitialize(Node n, + bool processInitialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) override; /** Tries to build new candidate solutions with new enumerated expressions diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 10c0104bc..ac3adb36a 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -56,17 +56,24 @@ class SygusModule SygusModule(QuantifiersEngine* qe, SynthConjecture* p); virtual ~SygusModule() {} /** initialize + * + * This function initializes the module for solving the given conjecture. This + * typically involves registering enumerators (for constructing terms) via + * calls to TermDbSygus::registerEnumerator. + * + * This function returns true if this module will take responsibility for + * constructing candidates for the given conjecture. + * + * conj is the synthesis conjecture (prior to deep-embedding). * * n is the "base instantiation" of the deep-embedding version of the * synthesis conjecture under candidates (see SynthConjecture::d_base_inst). * * This function may add lemmas to the argument lemmas, which should be * sent out on the output channel of quantifiers by the caller. - * - * This function returns true if this module will take responsibility for - * constructing candidates for the given conjecture. */ - virtual bool initialize(Node n, + virtual bool initialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) = 0; /** get term list diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 2ab51f1fb..c76082b02 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -144,7 +144,8 @@ bool SygusPbe::collectExamples(Node n, return true; } -bool SygusPbe::initialize(Node n, +bool SygusPbe::initialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) { diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index e82ce01da..258fe017b 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -107,7 +107,8 @@ class SygusPbe : public SygusModule * of an enumerator is not ITE if it is being used to construct * return values for decision trees. */ - bool initialize(Node n, + bool initialize(Node conj, + Node n, const std::vector& candidates, std::vector& lemmas) override; /** get term list diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index aabc2f1f3..97e5a5338 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -191,7 +191,8 @@ void SynthConjecture::assign(Node q) d_ceg_proc->initialize(d_base_inst, d_candidates); for (unsigned i = 0, size = d_modules.size(); i < size; i++) { - if (d_modules[i]->initialize(d_base_inst, d_candidates, guarded_lemmas)) + if (d_modules[i]->initialize( + d_simp_quant, d_base_inst, d_candidates, guarded_lemmas)) { d_master = d_modules[i]; break;