From 1079b96f2d06ddd9a8010f165250cb3aac54759d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 11 Apr 2019 17:31:53 -0700 Subject: remove experiments --- src/expr/expr_template.cpp | 1 + src/theory/strings/theory_strings.cpp | 140 +++-------------------- src/theory/strings/theory_strings.h | 2 - src/theory/strings/theory_strings_preprocess.cpp | 1 - 4 files changed, 20 insertions(+), 124 deletions(-) diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index b71d334da..d6a6f47bb 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -211,6 +211,7 @@ public: // Temporarily set the node manager to nullptr; this gets around // a check that mkVar isn't called internally + NodeManagerScope nullScope(nullptr); to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { // skolems are only available at the Node level (not the Expr level) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 50a14a5ab..6333bfee1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -127,9 +127,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_cardinality_lits(u), d_curr_cardinality(c, 0), d_sslds(nullptr), - d_strategy_init(false), - d_userContext(u), - d_satContext(c) + d_strategy_init(false) { setupExtTheory(); getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); @@ -505,7 +503,6 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd) << "Process reduction for " << n << ", pol = " << pol << std::endl; if (k == STRING_STRCTN && pol == 1) { - //std::cout << "REDUCING: " << n << " " << effort << std::endl; Node x = n[0]; Node s = n[1]; // positive contains reduces to a equality @@ -1609,7 +1606,6 @@ void TheoryStrings::checkExtfEval( int effort ) { std::vector< Node > sterms; std::vector< std::vector< Node > > exp; getExtTheory()->getSubstitutedTerms( effort, terms, sterms, exp ); - //std::cout << "checkExtfEval " << effort << " " << terms << std::endl; for( unsigned i=0; imkNode(kind::STRING_STRCTN, to_reduce[0], to_reduce[1]), - einfo, - effort); - checkExtfInference( - n, - nm->mkNode(kind::STRING_STRCTN, to_reduce[1], to_reduce[0]), - einfo, - effort); - } - else - { - checkExtfInference(n, to_reduce, einfo, effort); - } + checkExtfInference(n, to_reduce, einfo, effort); if( Trace.isOn("strings-extf-list") ){ Trace("strings-extf-list") << " * " << to_reduce; if (!einfo.d_const.isNull()) @@ -1786,7 +1762,6 @@ void TheoryStrings::checkExtfEval( int effort ) { } } d_has_extf = has_nreduce; - //std::cout << "/checkExtfEval " << effort << std::endl; } void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int effort ){ @@ -1826,13 +1801,10 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef if (nr.getKind() == STRING_STRCTN) { - Node nrr[2]; - nrr[0] = getRepresentative(nr[0]); - nrr[1] = getRepresentative(nr[1]); Assert(in.d_const.isConst()); bool pol = in.d_const.getConst(); - if ((pol && nrr[1].getKind() == STRING_CONCAT) - || (!pol && nrr[0].getKind() == STRING_CONCAT)) + if ((pol && nr[1].getKind() == STRING_CONCAT) + || (!pol && nr[0].getKind() == STRING_CONCAT)) { // If str.contains( x, str.++( y1, ..., yn ) ), // we may infer str.contains( x, y1 ), ..., str.contains( x, yn ) @@ -1852,9 +1824,9 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef int index = pol ? 1 : 0; std::vector children; - children.push_back(nrr[0]); - children.push_back(nrr[1]); - for (const Node& nrc : nrr[index]) + children.push_back(nr[0]); + children.push_back(nr[1]); + for (const Node& nrc : nr[index]) { children[index] = nrc; Node conc = nm->mkNode(STRING_STRCTN, children); @@ -1878,17 +1850,16 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } else { - if (std::find(d_extf_info_tmp[nrr[0]].d_ctn[pol].begin(), - d_extf_info_tmp[nrr[0]].d_ctn[pol].end(), - nrr[1]) - == d_extf_info_tmp[nrr[0]].d_ctn[pol].end()) + if (std::find(d_extf_info_tmp[nr[0]].d_ctn[pol].begin(), + d_extf_info_tmp[nr[0]].d_ctn[pol].end(), + nr[1]) + == d_extf_info_tmp[nr[0]].d_ctn[pol].end()) { - Trace("strings-extf-debug") << " store contains info : " << nrr[0] - << " " << pol << " " << nrr[1] << std::endl; + Trace("strings-extf-debug") << " store contains info : " << nr[0] + << " " << pol << " " << nr[1] << std::endl; // Store s (does not) contains t, since nr = (~)contains( s, t ) holds. - AlwaysAssert(std::find(d_extf_info_tmp[nrr[0]].d_ctn[pol].begin(), d_extf_info_tmp[nrr[0]].d_ctn[pol].end(), nrr[1]) == d_extf_info_tmp[nrr[0]].d_ctn[pol].end()); - d_extf_info_tmp[nrr[0]].d_ctn[pol].push_back(nrr[1]); - d_extf_info_tmp[nrr[0]].d_ctn_from[pol].push_back(n); + d_extf_info_tmp[nr[0]].d_ctn[pol].push_back(nr[1]); + d_extf_info_tmp[nr[0]].d_ctn_from[pol].push_back(n); // Do transistive closure on contains, e.g. // if contains( s, t ) and ~contains( s, r ), then ~contains( t, r ). @@ -1909,13 +1880,13 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef // we prefer being lazy: only if ~contains( s, r ) appears later do we // infer ~contains( t, r ), which suffices to show a conflict. bool opol = !pol; - for (unsigned i = 0, size = d_extf_info_tmp[nrr[0]].d_ctn[opol].size(); + for (unsigned i = 0, size = d_extf_info_tmp[nr[0]].d_ctn[opol].size(); i < size; i++) { - Node onr = d_extf_info_tmp[nrr[0]].d_ctn[opol][i]; + Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i]; Node conc = - nm->mkNode(STRING_STRCTN, pol ? nrr[1] : onr, pol ? onr : nrr[1]); + nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]); conc = Rewriter::rewrite(conc); conc = conc.negate(); bool do_infer = false; @@ -1934,7 +1905,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef { std::vector exp_c; exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end()); - Node ofrom = d_extf_info_tmp[nrr[0]].d_ctn_from[opol][i]; + Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i]; Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end()); exp_c.insert(exp_c.end(), d_extf_info_tmp[ofrom].d_exp.begin(), @@ -1942,77 +1913,6 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef sendInference(exp_c, conc, "CTN_Trans"); } } - - for (const auto& kv : d_extf_info_tmp) - { - if (kv.second.d_ctn.find(opol) != kv.second.d_ctn.end()) - { - auto it = std::find(kv.second.d_ctn.at(opol).begin(), - kv.second.d_ctn.at(opol).end(), - nrr[1]); - if (it != kv.second.d_ctn.at(opol).end()) - { - Node conc = nm->mkNode(STRING_STRCTN, - pol ? kv.first : nrr[0], - pol ? nrr[0] : kv.first); - conc = Rewriter::rewrite(conc); - conc = conc.negate(); - bool do_infer = false; - bool pol = conc.getKind() != NOT; - Node lit = pol ? conc : conc[0]; - if (lit.getKind() == EQUAL) - { - do_infer = pol ? !areEqual(lit[0], lit[1]) - : !areDisequal(lit[0], lit[1]); - } - else - { - do_infer = !areEqual(lit, pol ? d_true : d_false); - } - // std::cout << effort << " Do not reduce " << " -> " - // << lit << " " << getExtTheory()->isActive(lit) - // << std::endl; - // std::cout << "LEVEL: " << d_userContext->getLevel() << " " - // << d_satContext->getLevel() << std::endl; - if (false && hasTerm(lit)) { - std::vector exp_c(in.d_exp.begin(), in.d_exp.end()); - size_t i = std::distance(kv.second.d_ctn.at(opol).begin(), it); - Node ofrom = d_extf_info_tmp[kv.first].d_ctn_from[opol][i]; - Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end()); - exp_c.insert(exp_c.end(), - d_extf_info_tmp[ofrom].d_exp.begin(), - d_extf_info_tmp[ofrom].d_exp.end()); - if (false /*true*/) //d_userContext->getLevel() + 1 == d_satContext->getLevel()) - { - // std::cout << effort << " Do not reduce " << exp_c << " -> " - // << lit << " " << getExtTheory()->isActive(lit) - // << std::endl; - // std::cout << "LEVEL: " << d_userContext->getLevel() << " " - // << d_satContext->getLevel() << std::endl; - } - getExtTheory()->markReduced(lit); - } - if (getExtTheory()->isActive(lit)) //do_infer /* || (hasTerm(lit) && !getExtTheory()->isActive(lit))*/) - { - std::vector exp_c(in.d_exp.begin(), in.d_exp.end()); - size_t i = std::distance(kv.second.d_ctn.at(opol).begin(), it); - Node ofrom = d_extf_info_tmp[kv.first].d_ctn_from[opol][i]; - Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end()); - exp_c.insert(exp_c.end(), - d_extf_info_tmp[ofrom].d_exp.begin(), - d_extf_info_tmp[ofrom].d_exp.end()); - // std::cout << exp_c << " -> " << conc << std::endl; - sendInference(exp_c, conc, "CTN_Trans2"); - getExtTheory()->markReduced(lit); - } else { - // std::cout << effort << " Do not reduce " - // << lit << " " << getExtTheory()->isActive(lit) - // << std::endl; - getExtTheory()->markReduced(lit); - } - } - } - } } else { @@ -4958,7 +4858,6 @@ void TheoryStrings::initializeStrategy() } if (options::stringExp() && !options::stringGuessModel()) { - addStrategyStep(CHECK_EXTF_EVAL, 2); addStrategyStep(CHECK_EXTF_REDUCTION, 2); } addStrategyStep(CHECK_MEMBERSHIP); @@ -4968,7 +4867,6 @@ void TheoryStrings::initializeStrategy() { step_begin[EFFORT_LAST_CALL] = d_infer_steps.size(); // these two steps are run in parallel - addStrategyStep(CHECK_EXTF_EVAL, 2); addStrategyStep(CHECK_EXTF_REDUCTION, 2, false); addStrategyStep(CHECK_EXTF_EVAL, 3); step_end[EFFORT_LAST_CALL] = d_infer_steps.size() - 1; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 58f651e84..b3cb323ae 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -1108,8 +1108,6 @@ private: void runStrategy(unsigned sbegin, unsigned send); //-----------------------end representation of the strategy - context::Context* d_userContext; - context::Context* d_satContext; };/* class TheoryStrings */ }/* CVC4::theory::strings namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index de3cdb33a..6ceeff6f2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -487,7 +487,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // Thus, replaceall( x, y, z ) = rpaw retNode = rpaw; } else if( t.getKind() == kind::STRING_STRCTN ){ - //std::cout << "NREDUCING " << t << std::endl; Node x = t[0]; Node s = t[1]; //negative contains reduces to existential -- cgit v1.2.3