From dbc501933c7e77fc61dcf6092050d3bb67ba5a49 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Apr 2018 09:53:41 -0500 Subject: [PATCH] Remove nl solve subs option. (#1803) --- src/options/arith_options.toml | 9 - src/theory/arith/nonlinear_extension.cpp | 413 ----------------------- 2 files changed, 422 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 4f68d1689..1cccf0884 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -477,15 +477,6 @@ header = "options/arith_options.h" read_only = true help = "do rewrites in non-linear solver" -[[option]] - name = "nlExtSolveSubs" - category = "regular" - long = "nl-ext-solve-subs" - type = "bool" - default = "false" - read_only = true - help = "do solving for determining constant substitutions" - [[option]] name = "nlExtPurify" category = "regular" diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 0d9eb3a5f..b43f0d094 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -68,12 +68,6 @@ unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value) { return (it == a.end()) ? value : it->second; } -// Returns map[key] if key is in map or Node::null() otherwise. -Node getNodeOrNull(const std::map& map, Node key) { - std::map::const_iterator it = map.find(key); - return (it == map.end()) ? Node::null() : it->second; -} - // Returns true if for any key then a[key] <= b[key] where the value for any key // not present is interpreted as 0. bool isSubset(const NodeMultiset& a, const NodeMultiset& b) { @@ -116,63 +110,6 @@ void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) { Trace(c) << t << " " << type << " " << rhs; } -struct SubstitutionConstResult { - // The resulting term of the substitution. - Node term; - - // ? - std::vector const_exp; - - // ?? - // A term sum[i] for which for rep_sum[i] not in rep_to_const. - Node variable_term; -}; /* struct SubstitutionConstResult */ - -SubstitutionConstResult getSubstitutionConst( - Node n, Node n_rsu, Node rsu_exp, - const std::vector& sum, const std::vector& rep_sum, - const std::map& rep_to_const, - const std::map& rep_to_const_exp, - const std::map& rep_to_const_base) { - Assert(sum.size() == rep_sum.size()); - - SubstitutionConstResult result; - - std::vector vars; - std::vector subs; - std::set rep_exp_proc; - for (unsigned i = 0; i < rep_sum.size(); i++) { - Node cr = rep_sum[i]; - Node const_of_cr = getNodeOrNull(rep_to_const, cr); - if (const_of_cr.isNull()) { - result.variable_term = sum[i]; - continue; - } - Assert(!const_of_cr.isNull()); - Node const_base_of_cr = getNodeOrNull(rep_to_const_base, cr); - Assert(!const_base_of_cr.isNull()); - if (const_base_of_cr != sum[i]) { - result.const_exp.push_back(const_base_of_cr.eqNode(sum[i])); - } - if (rep_exp_proc.find(cr) == rep_exp_proc.end()) { - rep_exp_proc.insert(cr); - Node const_exp = getNodeOrNull(rep_to_const_exp, cr); - if (!const_exp.isNull()) { - result.const_exp.push_back(const_exp); - } - } - vars.push_back(sum[i]); - subs.push_back(const_of_cr); - } - if( n!=n_rsu && !rsu_exp.isNull() ){ - result.const_exp.push_back( rsu_exp ); - } - Node substituted = - n_rsu.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - result.term = Rewriter::rewrite(substituted); - return result; -} - struct SortNonlinearExtension { SortNonlinearExtension() : d_nla(NULL), d_order_type(0), d_reverse_order(false) {} @@ -291,349 +228,6 @@ void NonlinearExtension::registerMonomialSubset(Node a, Node b) { << ", difference is " << mult_term << std::endl; } -class NonLinearExtentionSubstitutionSolver { - public: - NonLinearExtentionSubstitutionSolver(const eq::EqualityEngine* ee) - : d_ee(ee) {} - - bool solve(const std::vector& vars, std::vector* subs, - std::map >* exp, - std::map >* rep_to_subs_index); - - private: - bool setSubstitutionConst( - const std::vector& vars, Node r, Node r_c, Node r_cb, - const std::vector& r_c_exp, std::vector* subs, - std::map >* exp, - std::map >* rep_to_subs_index); - - const eq::EqualityEngine* d_ee; - - std::map d_rep_sum_unique; - std::map d_rep_sum_unique_exp; - - std::map d_rep_to_const; - std::map d_rep_to_const_exp; - std::map d_rep_to_const_base; - - // key in term_to_sum iff key in term_to_rep_sum. - std::map > d_term_to_sum; - std::map > d_term_to_rep_sum; - std::map d_term_to_nconst_rep_count; - - std::map > d_reps_to_parent_terms; - std::map > d_reps_to_terms; -}; - -bool NonLinearExtentionSubstitutionSolver::solve( - const std::vector& vars, std::vector* subs, - std::map >* exp, - std::map >* rep_to_subs_index) { - // std::map rep_to_const; - // std::map rep_to_const_exp; - // std::map rep_to_const_base; - - // std::map > term_to_sum; - // std::map > term_to_rep_sum; - // std::map term_to_nconst_rep_count; - // std::map > reps_to_parent_terms; - // std::map > reps_to_terms; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_ee); - - bool retVal = false; - while (!eqcs_i.isFinished() && !rep_to_subs_index->empty()) { - Node r = (*eqcs_i); - if (r.getType().isReal()) { - Trace("nl-subs-debug") - << "Process equivalence class " << r << "..." << std::endl; - Node r_c; - Node r_cb; - std::vector r_c_exp; - if (r.isConst()) { - r_c = r; - r_cb = r; - } - // scan the class - eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_ee); - while (!eqc_i.isFinished()) { - Node n = (*eqc_i); - if (!n.isConst()) { - Trace("nl-subs-debug") << "Look at term : " << n << std::endl; - std::map msum; - if (ArithMSum::getMonomialSum(n, msum)) - { - int nconst_count = 0; - bool evaluatable = true; - //first, collect sums of equal terms - std::map< Node, Node > rep_to_mon; - std::vector< Node > subs_rm; - std::vector< Node > vars_rm; - std::vector< Node > exp_rm; - for (std::map::iterator itm = msum.begin(); - itm != msum.end(); ++itm) { - if (!itm->first.isNull()) { - if (d_ee->hasTerm(itm->first)) { - Node cr = d_ee->getRepresentative(itm->first); - std::map< Node, Node >::iterator itrm = rep_to_mon.find( cr ); - if( itrm==rep_to_mon.end() ){ - rep_to_mon[cr] = itm->first; - }else{ - vars_rm.push_back( itm->first ); - subs_rm.push_back( itrm->second ); - exp_rm.push_back( itm->first.eqNode( itrm->second ) ); - } - } - }else{ - Trace("nl-subs-debug") - << "...is not evaluatable due to monomial " << itm->first - << std::endl; - evaluatable = false; - break; - } - } - if( evaluatable ){ - bool success = true; - if( !vars_rm.empty() ){ - Node ns = n.substitute( vars_rm.begin(), vars_rm.end(), subs_rm.begin(), subs_rm.end() ); - ns = Rewriter::rewrite( ns ); - if( ns.isConst() ){ - success = false; - if( r_c.isNull() ){ - r_c = ns; - r_cb = n; - r_c_exp.insert( r_c_exp.end(), exp_rm.begin(), exp_rm.end() ); - } - }else{ - //recompute the monomial - msum.clear(); - if (!ArithMSum::getMonomialSum(ns, msum)) - { - success = false; - }else{ - d_rep_sum_unique_exp[n] = - exp_rm.size() == 1 - ? exp_rm[0] - : NodeManager::currentNM()->mkNode(AND, exp_rm); - d_rep_sum_unique[n] = ns; - } - } - }else{ - d_rep_sum_unique[n] = n; - } - if( success ){ - for (std::map::iterator itm = msum.begin(); - itm != msum.end(); ++itm) { - if (!itm->first.isNull()) { - if (d_ee->hasTerm(itm->first)) { - Trace("nl-subs-debug") - << " ...monomial " << itm->first << std::endl; - Node cr = d_ee->getRepresentative(itm->first); - d_term_to_sum[n].push_back(itm->first); - d_term_to_rep_sum[n].push_back(cr); - if (!Contains(d_rep_to_const, cr)) { - if (!IsInVector(d_reps_to_parent_terms[cr], n)) { - d_reps_to_parent_terms[cr].push_back(n); - nconst_count++; - } - } - } else { - Assert( false ); - } - } - } - if (evaluatable) { - Trace("nl-subs-debug") - << " ...term has " << nconst_count - << " unique non-constant represenative children." - << std::endl; - if (nconst_count == 0) { - if (r_c.isNull()) { - const SubstitutionConstResult result = getSubstitutionConst( - n, d_rep_sum_unique[n], d_rep_sum_unique_exp[n], - d_term_to_sum[n], d_term_to_rep_sum[n], d_rep_to_const, - d_rep_to_const_exp, d_rep_to_const_base); - r_c_exp.insert(r_c_exp.end(), result.const_exp.begin(), - result.const_exp.end()); - r_c = result.term; - r_cb = n; - Assert(result.variable_term.isNull()); - Assert(r_c.isConst()); - } - } else { - d_reps_to_terms[r].push_back(n); - d_term_to_nconst_rep_count[n] = nconst_count; - } - } - } - } - } else { - Trace("nl-subs-debug") - << "...could not get monomial sum " << std::endl; - } - } - ++eqc_i; - } - if (!r_c.isNull()) { - setSubstitutionConst(vars, r, r_c, r_cb, r_c_exp, subs, exp, - rep_to_subs_index); - } - } - ++eqcs_i; - } - return retVal; -} - -bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst( - const std::vector& vars, Node r, Node r_c, Node r_cb, - const std::vector& r_c_exp, std::vector* subs, - std::map >* exp, - std::map >* rep_to_subs_index) { - Trace("nl-subs-debug") << "Set constant equivalence class : " << r << " -> " - << r_c << std::endl; - bool retVal = false; - - d_rep_to_const[r] = r_c; - Node expn; - if (!r_c_exp.empty()) { - expn = r_c_exp.size() == 1 ? r_c_exp[0] - : NodeManager::currentNM()->mkNode(AND, r_c_exp); - Trace("nl-subs-debug") << "...explanation is " << expn << std::endl; - d_rep_to_const_exp[r] = expn; - } - d_rep_to_const_base[r] = r_cb; - - std::map >::const_iterator iti = - rep_to_subs_index->find(r); - if (iti != rep_to_subs_index->end()) { - for (unsigned i = 0; i < iti->second.size(); i++) { - int ii = iti->second[i]; - (*subs)[ii] = r_c; - std::vector& exp_var_ii = (*exp)[vars[ii]]; - exp_var_ii.clear(); - if (!expn.isNull()) { - exp_var_ii.push_back(expn); - } - if (vars[ii] != r_cb) { - exp_var_ii.push_back(vars[ii].eqNode(r_cb)); - } - } - retVal = true; - rep_to_subs_index->erase(r); - if (rep_to_subs_index->empty()) { - return retVal; - } - } - - // new inferred constants - std::map new_const; - std::map > new_const_exp; - - // parent terms now evaluate to constants - std::map >::const_iterator itrp = - d_reps_to_parent_terms.find(r); - if (itrp != d_reps_to_parent_terms.end()) { - // Trace("nl-subs-debug") << "Look at " << itrp->second.size() << " parent - // terms." << std::endl; - for (unsigned i = 0; i < itrp->second.size(); i++) { - Node m = itrp->second[i]; - d_term_to_nconst_rep_count[m]--; - Node r = d_ee->getRepresentative(m); - if (d_term_to_nconst_rep_count[m] == 0) { - if (!Contains(d_rep_to_const, r)) { - Trace("nl-subs-debug") << "...parent term " << m - << " evaluates to constant." << std::endl; - if (!Contains(new_const, m)) { - const SubstitutionConstResult result = getSubstitutionConst( - m, d_rep_sum_unique[m], d_rep_sum_unique_exp[m], - d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, - d_rep_to_const_exp, d_rep_to_const_base); - new_const_exp[m].insert(new_const_exp[m].end(), - result.const_exp.begin(), - result.const_exp.end()); - Node m_c = result.term; - // count should be accurate - Assert(result.variable_term.isNull()); - Assert(m_c.isConst()); - new_const[m] = m_c; - } - } - } else if (d_term_to_nconst_rep_count[m] == 1) { - // check if it is now univariate solved - if (Contains(d_rep_to_const, r)) { - Trace("nl-subs-debug") << "...parent term " << m - << " is univariate solved." << std::endl; - const SubstitutionConstResult result = getSubstitutionConst( - m, d_rep_sum_unique[m], d_rep_sum_unique_exp[m], - d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, - d_rep_to_const_exp, d_rep_to_const_base); - Node eq = (result.term).eqNode(d_rep_to_const[r]); - Node v_c = ArithMSum::solveEqualityFor(eq, result.variable_term); - if (!v_c.isNull()) { - Assert(v_c.isConst()); - if (Contains(new_const, result.variable_term)) { - new_const[result.variable_term] = v_c; - std::vector& explanation = - new_const_exp[result.variable_term]; - explanation.insert(explanation.end(), result.const_exp.begin(), - result.const_exp.end()); - if (m != d_rep_to_const_base[r]) { - explanation.push_back(m.eqNode(d_rep_to_const_base[r])); - } - } - } - } - } - } - } - - // equal univariate terms now solved - std::map >::iterator itt = d_reps_to_terms.find(r); - if (itt != d_reps_to_terms.end()) { - for (unsigned i = 0; i < itt->second.size(); i++) { - Node m = itt->second[i]; - if (d_term_to_nconst_rep_count[m] == 1) { - Trace("nl-subs-debug") - << "...term " << m << " is univariate solved." << std::endl; - const SubstitutionConstResult result = getSubstitutionConst( - m, d_rep_sum_unique[m], d_rep_sum_unique_exp[m], - d_term_to_sum[m], d_term_to_rep_sum[m], d_rep_to_const, - d_rep_to_const_exp, d_rep_to_const_base); - Node v = result.variable_term; - Node m_t = result.term; - Node eq = m_t.eqNode(r_c); - Node v_c = ArithMSum::solveEqualityFor(eq, v); - Trace("nl-subs-debug") << "Solved equality " << eq << " for " << v << ", got = " << v_c << std::endl; - if (!v_c.isNull()) { - Assert(v_c.isConst()); - if (new_const.find(v) == new_const.end()) { - new_const[v] = v_c; - new_const_exp[v].insert(new_const_exp[v].end(), - result.const_exp.begin(), - result.const_exp.end()); - if (m != r_cb) { - new_const_exp[v].push_back(m.eqNode(r_cb)); - } - } - } - } - } - } - - // now, process new inferred constants - for (std::map::iterator itn = new_const.begin(); - itn != new_const.end(); ++itn) { - Node m = itn->first; - Node r = d_ee->getRepresentative(m); - if (!Contains(d_rep_to_const, r)) { - if (setSubstitutionConst(vars, r, itn->second, m, new_const_exp[m], subs, - exp, rep_to_subs_index)) { - retVal = true; - } - } - } - return retVal; -} - bool NonlinearExtension::getCurrentSubstitution( int effort, const std::vector& vars, std::vector& subs, std::map >& exp) { @@ -660,13 +254,6 @@ bool NonlinearExtension::getCurrentSubstitution( } } - if (options::nlExtSolveSubs()) { - NonLinearExtentionSubstitutionSolver substitution_solver(d_ee); - if (substitution_solver.solve(vars, &subs, &exp, &rep_to_subs_index)) { - retVal = true; - } - } - // return true if the substitution is non-trivial return retVal; -- 2.30.2