diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 09:31:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-23 09:31:21 -0500 |
commit | 847f415d9bd9aa98470109fbdc37fd379a79cb4e (patch) | |
tree | 653841f3a0a8195743fa9cc31f7ef3f005e9c1ad /src/theory/quantifiers/sygus/cegis.cpp | |
parent | b58bdc9c5672430cf15914c64129136b24050152 (diff) |
Pass synthesis conjecture to sygus modules (#3212)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
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<Node>& candidates, std::vector<Node>& 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<Node>& candidates, std::vector<Node>& lemmas) { |