From 448a874adc9314d42a107b24654b155ba465e202 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Apr 2018 19:43:05 -0500 Subject: [PATCH] Make construct solution behavior specific to SygusIO (#1827) --- src/theory/quantifiers/sygus/sygus_unif.cpp | 54 +++---------------- src/theory/quantifiers/sygus/sygus_unif.h | 12 ----- .../quantifiers/sygus/sygus_unif_io.cpp | 50 ++++++++++++++++- src/theory/quantifiers/sygus/sygus_unif_io.h | 13 +++++ 4 files changed, 68 insertions(+), 61 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index ab2b06a82..9a017d21b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,10 +26,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusUnif::SygusUnif() - : d_qe(nullptr), d_tds(nullptr), d_check_sol(false), d_cond_count(0) -{ -} +SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {} SygusUnif::~SygusUnif() {} @@ -48,50 +45,11 @@ void SygusUnif::initialize(QuantifiersEngine* qe, Node SygusUnif::constructSolution() { - Node c = d_candidate; - if (!d_solution.isNull()) - { - // already has a solution - return d_solution; - } - // only check if an enumerator updated - if (d_check_sol) - { - Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count - << std::endl; - d_check_sol = false; - // try multiple times if we have done multiple conditions, due to - // non-determinism - Node vc; - for (unsigned i = 0; i <= d_cond_count; i++) - { - Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; - Node e = d_strategy.getRootEnumerator(); - // initialize a call to construct solution - initializeConstructSol(); - // call the virtual construct solution method - Node vcc = constructSol(e, role_equal, 1); - // if we constructed the solution, and we either did not previously have - // a solution, or the new solution is better (smaller). - if (!vcc.isNull() - && (vc.isNull() || (!vc.isNull() - && d_tds->getSygusTermSize(vcc) - < d_tds->getSygusTermSize(vc)))) - { - Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc - << std::endl; - Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; - vc = vcc; - } - } - if (!vc.isNull()) - { - d_solution = vc; - return vc; - } - Trace("sygus-pbe") << "...failed to solve." << std::endl; - } - return Node::null(); + // initialize a call to construct solution + initializeConstructSol(); + // call the virtual construct solution method + Node e = d_strategy.getRootEnumerator(); + return constructSol(e, role_equal, 1); } Node SygusUnif::constructBestSolvedTerm(const std::vector& solved) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 728d613b2..beb2023f9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -99,18 +99,6 @@ class SygusUnif std::vector& vals, bool pol = true); //-----------------------end debug printing - - - /** - * Whether we will try to construct solution on the next call to - * constructSolution. This flag is set to true when we successfully - * register a new value for an enumerator. - */ - bool d_check_sol; - /** The number of values we have enumerated for all enumerators. */ - unsigned d_cond_count; - /** The solution for the function of this class, if one has been found */ - Node d_solution; /** the candidate for this class */ Node d_candidate; /** maps a function-to-synthesize to the above information */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index abdaf0cb2..7a134b1c0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -459,7 +459,7 @@ void SubsumeTrie::getLeaves(const std::vector& vals, getLeavesInternal(vals, pol, v, 0, -2); } -SygusUnifIo::SygusUnifIo() +SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -677,6 +677,54 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) lemmas.push_back(exp_exc); } +Node SygusUnifIo::constructSolution() +{ + Node c = d_candidate; + if (!d_solution.isNull()) + { + // already has a solution + return d_solution; + } + // only check if an enumerator updated + if (d_check_sol) + { + Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count + << std::endl; + d_check_sol = false; + // try multiple times if we have done multiple conditions, due to + // non-determinism + Node vc; + for (unsigned i = 0; i <= d_cond_count; i++) + { + Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; + // initialize a call to construct solution + initializeConstructSol(); + // call the virtual construct solution method + Node e = d_strategy.getRootEnumerator(); + Node vcc = constructSol(e, role_equal, 1); + // if we constructed the solution, and we either did not previously have + // a solution, or the new solution is better (smaller). + if (!vcc.isNull() + && (vc.isNull() || (!vc.isNull() + && d_tds->getSygusTermSize(vcc) + < d_tds->getSygusTermSize(vc)))) + { + Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc + << std::endl; + Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + vc = vcc; + } + } + if (!vc.isNull()) + { + d_solution = vc; + return vc; + } + Trace("sygus-pbe") << "...failed to solve." << std::endl; + } + return Node::null(); +} + // ------------------------------------ solution construction from enumeration bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 94fb2e754..276cc9da2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -271,6 +271,9 @@ class SygusUnifIo : public SygusUnif Node v, std::vector& lemmas) override; + /** Construct solution */ + virtual Node constructSolution() override; + /** add example * * This adds input -> output to the specification for f. The arity of @@ -281,6 +284,16 @@ class SygusUnifIo : public SygusUnif void addExample(const std::vector& input, Node output); protected: + /** + * Whether we will try to construct solution on the next call to + * constructSolution. This flag is set to true when we successfully + * register a new value for an enumerator. + */ + bool d_check_sol; + /** The number of values we have enumerated for all enumerators. */ + unsigned d_cond_count; + /** The solution for the function of this class, if one has been found */ + Node d_solution; /** true and false nodes */ Node d_true; Node d_false; -- 2.30.2