diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-27 19:43:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-27 19:43:05 -0500 |
commit | 448a874adc9314d42a107b24654b155ba465e202 (patch) | |
tree | 72a9ed78c241952f645376e07b782b3bf42aaee4 /src/theory/quantifiers/sygus/sygus_unif.cpp | |
parent | 5b2c33bf0bd968b970d5f228f291477d20b751df (diff) |
Make construct solution behavior specific to SygusIO (#1827)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 54 |
1 files changed, 6 insertions, 48 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<Node>& solved) |