From 3fe18c9d3b15e1c4a7bf23d54bf92e2ae27c6a80 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 May 2018 21:11:18 -0500 Subject: Initialize cegis unif strategy (#1861) --- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/quantifiers/sygus/sygus_unif_io.cpp') diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index eb607d2c3..8f2038d31 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -477,6 +477,8 @@ void SygusUnifIo::initialize(QuantifiersEngine* qe, d_ecache.clear(); d_candidate = funs[0]; SygusUnif::initialize(qe, funs, enums, lemmas); + // learn redundant operators based on the strategy + d_strategy[d_candidate].staticLearnRedundantOps(lemmas); } void SygusUnifIo::addExample(const std::vector& input, Node output) -- cgit v1.2.3