summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_pbe.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-23 09:31:21 -0500
committerGitHub <noreply@github.com>2019-08-23 09:31:21 -0500
commit847f415d9bd9aa98470109fbdc37fd379a79cb4e (patch)
tree653841f3a0a8195743fa9cc31f7ef3f005e9c1ad /src/theory/quantifiers/sygus/sygus_pbe.cpp
parentb58bdc9c5672430cf15914c64129136b24050152 (diff)
Pass synthesis conjecture to sygus modules (#3212)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.cpp3
1 files changed, 2 insertions, 1 deletions
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<Node>& candidates,
std::vector<Node>& lemmas)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback