From 43e02cedf0e2a2700a2ace23cf85cff9bb242f13 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 29 Nov 2018 00:17:14 -0600 Subject: [PATCH] Combine sygus stream with PBE (#2726) --- src/smt/smt_engine.cpp | 9 ++-- src/theory/quantifiers/sygus/sygus_unif.cpp | 36 +++++++++++++- src/theory/quantifiers/sygus/sygus_unif.h | 9 ++++ .../quantifiers/sygus/sygus_unif_io.cpp | 49 ++++++++++++++----- src/theory/quantifiers/sygus/sygus_unif_io.h | 2 + 5 files changed, 88 insertions(+), 17 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1de3e3756..a0939f4db 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1938,13 +1938,14 @@ void SmtEngine::setDefaults() { // Streaming is incompatible with techniques that focus the search towards // finding a single solution. This currently includes the PBE solver and // static template inference for invariant synthesis. - if (!options::sygusSymBreakPbe.wasSetByUser()) - { - options::sygusSymBreakPbe.set(false); - } if (!options::sygusUnifPbe.wasSetByUser()) { options::sygusUnifPbe.set(false); + // also disable PBE-specific symmetry breaking unless PBE was enabled + if (!options::sygusSymBreakPbe.wasSetByUser()) + { + options::sygusSymBreakPbe.set(false); + } } if (!options::sygusInvTemplMode.wasSetByUser()) { diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index a4f276792..5d7017a1c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,7 +26,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {} +SygusUnif::SygusUnif() + : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false) +{ +} SygusUnif::~SygusUnif() {} void SygusUnif::initializeCandidate( @@ -42,9 +45,40 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } +Node SygusUnif::getMinimalTerm(const std::vector& terms) +{ + unsigned minSize = 0; + Node minTerm; + std::map::iterator it; + for (const Node& n : terms) + { + it = d_termToSize.find(n); + unsigned ssize = 0; + if (it == d_termToSize.end()) + { + ssize = d_tds->getSygusTermSize(n); + d_termToSize[n] = ssize; + } + else + { + ssize = it->second; + } + if (minTerm.isNull() || ssize < minSize) + { + minTerm = n; + minSize = ssize; + } + } + return minTerm; +} + Node SygusUnif::constructBestSolvedTerm(Node e, const std::vector& solved) { Assert(!solved.empty()); + if (d_enableMinimality) + { + return getMinimalTerm(solved); + } return solved[0]; } diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 67e798854..0784644f8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -181,6 +181,15 @@ class SygusUnif const std::map& total_inc, const std::map >& incr); //------------------------------ end constructing solutions + /** map terms to their sygus size */ + std::map d_termToSize; + /** + * Whether to ensure terms selected by the above methods lead to minimal + * solutions. + */ + bool d_enableMinimality; + /** returns the term whose sygus size is minimal among those in terms */ + Node getMinimalTerm(const std::vector& terms); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 6daeb1706..89619639d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -238,11 +238,14 @@ Node SubsumeTrie::addTermInternal(Node t, if (!d_term.isNull()) { subsumed.push_back(d_term); - if (!checkExistsOnly) - { - // remove it if checkExistsOnly = false - d_term = Node::null(); - } + // If we are only interested in feasibility, we could set d_term to null + // here. However, d_term still could be useful, since it may be + // smaller than t and suffice as a solution under some condition. + // As a simple example, consider predicate synthesis and a case where we + // enumerate a C that is correct for all I/O points whose output is + // true. Then, C subsumes true. However, true may be preferred, e.g. + // to generate a solution ite( C, true, D ) instead of ite( C, C, D ), + // since true is conditionally correct under C, and is smaller than C. } } else @@ -470,6 +473,7 @@ void SubsumeTrie::getLeaves(const std::vector& vals, SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0), + d_sol_term_size(0), d_sol_cons_nondet(false), d_solConsUsingInfoGain(false) { @@ -771,7 +775,7 @@ bool SygusUnifIo::constructSolution(std::vector& sols, Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) { Node c = d_candidate; - if (!d_solution.isNull()) + if (!d_solution.isNull() && !options::sygusStream()) { // already has a solution return d_solution; @@ -782,10 +786,10 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count << std::endl; d_check_sol = false; + Node newSolution; d_solConsUsingInfoGain = false; // try multiple times if we have done multiple conditions, due to // non-determinism - unsigned sol_term_size = 0; for (unsigned i = 0; i <= d_cond_count; i++) { Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; @@ -800,19 +804,24 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) if (!vcc.isNull() && (d_solution.isNull() || (!d_solution.isNull() - && d_tds->getSygusTermSize(vcc) < sol_term_size))) + && d_tds->getSygusTermSize(vcc) < d_sol_term_size))) { Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc << std::endl; Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; d_solution = vcc; - sol_term_size = d_tds->getSygusTermSize(vcc); + newSolution = vcc; + d_sol_term_size = d_tds->getSygusTermSize(vcc); + Trace("sygus-pbe-sol") + << "PBE solution size: " << d_sol_term_size << std::endl; // We've determined its feasible, now, enable information gain and // retry. We do this since information gain comes with an overhead, // and we want testing feasibility to be fast. if (!d_solConsUsingInfoGain) { + // we permanently enable information gain and minimality now d_solConsUsingInfoGain = true; + d_enableMinimality = true; i = 0; } } @@ -821,9 +830,9 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) break; } } - if (!d_solution.isNull()) + if (!newSolution.isNull()) { - return d_solution; + return newSolution; } Trace("sygus-pbe") << "...failed to solve." << std::endl; } @@ -1427,6 +1436,7 @@ Node SygusUnifIo::constructBestConditional(Node ce, // initially set minEntropy to > 1.0. double minEntropy = 2.0; unsigned bestIndex = 0; + int numEqual = 1; for (unsigned j = 0; j < nconds; j++) { // To compute the entropy for a condition C, for pair of terms (s, t), let @@ -1460,7 +1470,22 @@ Node SygusUnifIo::constructBestConditional(Node ce, } } Trace("sygus-sui-dt-igain") << "..." << entropySum << std::endl; - if (entropySum < minEntropy) + // either less, or equal and coin flip passes + bool doSet = false; + if (entropySum == minEntropy) + { + numEqual++; + if (Random::getRandom().pickWithProb(double(1) / double(numEqual))) + { + doSet = true; + } + } + else if (entropySum < minEntropy) + { + doSet = true; + numEqual = 1; + } + if (doSet) { minEntropy = entropySum; bestIndex = j; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 8fa8b95e1..2f87c0552 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -298,6 +298,8 @@ class SygusUnifIo : public SygusUnif unsigned d_cond_count; /** The solution for the function of this class, if one has been found */ Node d_solution; + /** the term size of the above solution */ + unsigned d_sol_term_size; /** * This flag is set to true if the solution construction was * non-deterministic with respect to failure/success. -- 2.30.2