From f038f308e044bd1e842996e891e3cb119825113a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 13 Dec 2018 12:03:16 -0600 Subject: [PATCH] Remove spurious map (#2750) --- .../quantifiers/sygus/sygus_unif_io.cpp | 150 ++++++++---------- 1 file changed, 68 insertions(+), 82 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 0b378875c..c9db62735 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1323,7 +1323,6 @@ Node SygusUnifIo::constructSol( Trace("sygus-sui-dt") << "...try STRATEGY " << strat << "..." << std::endl; - std::map look_ahead_solved_children; std::vector dt_children_cons; bool success = true; @@ -1338,108 +1337,95 @@ Node SygusUnifIo::constructSol( Trace("sygus-sui-dt") << "construct PBE child #" << sc << "..." << std::endl; Node rec_c; - std::map::iterator itla = - look_ahead_solved_children.find(sc); - if (itla != look_ahead_solved_children.end()) + + std::pair& cenum = etis->d_cenum[sc]; + + // update the context + std::vector prev; + if (strat == strat_ITE && sc > 0) { - rec_c = itla->second; - indent("sygus-sui-dt-debug", ind + 1); - Trace("sygus-sui-dt-debug") - << "ConstructPBE: look ahead solved : " - << d_tds->sygusToBuiltin(rec_c) << std::endl; + EnumCache& ecache_cond = d_ecache[split_cond_enum]; + Assert(set_split_cond_res_index); + Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); + prev = x.d_vals; + x.updateContext(this, + ecache_cond.d_enum_vals_res[split_cond_res_index], + sc == 1); + // return value of above call may be false in corner cases where we + // must choose a non-separating condition to traverse to another + // strategy node } - else - { - std::pair& cenum = etis->d_cenum[sc]; - // update the context - std::vector prev; - if (strat == strat_ITE && sc > 0) - { - EnumCache& ecache_cond = d_ecache[split_cond_enum]; - Assert(set_split_cond_res_index); - Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); - prev = x.d_vals; - x.updateContext(this, - ecache_cond.d_enum_vals_res[split_cond_res_index], - sc == 1); - // return value of above call may be false in corner cases where we - // must choose a non-separating condition to traverse to another - // strategy node - } - - // recurse - if (strat == strat_ITE && sc == 0) - { - Node ce = cenum.first; + // recurse + if (strat == strat_ITE && sc == 0) + { + Node ce = cenum.first; - EnumCache& ecache_child = d_ecache[ce]; + EnumCache& ecache_child = d_ecache[ce]; - // get the conditionals in the current context : they must be - // distinguishable - std::map > possible_cond; - std::map solved_cond; // stores branch - ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); + // get the conditionals in the current context : they must be + // distinguishable + std::map > possible_cond; + std::map solved_cond; // stores branch + ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); - std::map>::iterator itpc = - possible_cond.find(0); - if (itpc != possible_cond.end()) + std::map>::iterator itpc = + possible_cond.find(0); + if (itpc != possible_cond.end()) + { + if (Trace.isOn("sygus-sui-dt-debug")) { - if (Trace.isOn("sygus-sui-dt-debug")) + indent("sygus-sui-dt-debug", ind + 1); + Trace("sygus-sui-dt-debug") + << "PBE : We have " << itpc->second.size() + << " distinguishable conditionals:" << std::endl; + for (Node& cond : itpc->second) { - indent("sygus-sui-dt-debug", ind + 1); + indent("sygus-sui-dt-debug", ind + 2); Trace("sygus-sui-dt-debug") - << "PBE : We have " << itpc->second.size() - << " distinguishable conditionals:" << std::endl; - for (Node& cond : itpc->second) - { - indent("sygus-sui-dt-debug", ind + 2); - Trace("sygus-sui-dt-debug") - << d_tds->sygusToBuiltin(cond) << std::endl; - } - } - if (rec_c.isNull()) - { - rec_c = constructBestConditional(ce, itpc->second); - Assert(!rec_c.isNull()); - indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") - << "PBE: ITE strategy : choose best conditional " - << d_tds->sygusToBuiltin(rec_c) << std::endl; + << d_tds->sygusToBuiltin(cond) << std::endl; } } - else + if (rec_c.isNull()) { - // TODO (#1250) : degenerate case where children have different - // types? + rec_c = constructBestConditional(ce, itpc->second); + Assert(!rec_c.isNull()); indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " - "cannot find a distinguishable condition" - << std::endl; - } - if (!rec_c.isNull()) - { - Assert(ecache_child.d_enum_val_to_index.find(rec_c) - != ecache_child.d_enum_val_to_index.end()); - split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; - set_split_cond_res_index = true; - split_cond_enum = ce; - Assert(split_cond_res_index - < ecache_child.d_enum_vals_res.size()); + Trace("sygus-sui-dt") + << "PBE: ITE strategy : choose best conditional " + << d_tds->sygusToBuiltin(rec_c) << std::endl; } } else { - did_recurse = true; - rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); + // TODO (#1250) : degenerate case where children have different + // types? + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition" + << std::endl; } - - // undo update the context - if (strat == strat_ITE && sc > 0) + if (!rec_c.isNull()) { - x.d_vals = prev; + Assert(ecache_child.d_enum_val_to_index.find(rec_c) + != ecache_child.d_enum_val_to_index.end()); + split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; + set_split_cond_res_index = true; + split_cond_enum = ce; + Assert(split_cond_res_index + < ecache_child.d_enum_vals_res.size()); } } + else + { + did_recurse = true; + rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); + } + // undo update the context + if (strat == strat_ITE && sc > 0) + { + x.d_vals = prev; + } if (!rec_c.isNull()) { dt_children_cons.push_back(rec_c); -- 2.30.2