summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis_unif.cpp
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2018-04-28 08:11:09 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-04-28 08:11:09 -0500
commit6cdf6fb87a48c04b72722382f43b7fded0b97778 (patch)
tree41bac2c14074fef6fdc237ba4b900d8745d7f730 /src/theory/quantifiers/sygus/cegis_unif.cpp
parent448a874adc9314d42a107b24654b155ba465e202 (diff)
Initial implementation of SygusUnifRL (#1829)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index f7d970ddf..7794ec912 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -130,6 +130,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
/* build candidate solution */
Assert(candidates.size() == 1);
Node vc = d_sygus_unif.constructSolution();
+ Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
if (vc.isNull())
{
return false;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback