return (it == a.end()) ? value : it->second;
}
-// Returns map[key] if key is in map or Node::null() otherwise.
-Node getNodeOrNull(const std::map<Node, Node>& map, Node key) {
- std::map<Node, Node>::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) {
Trace(c) << t << " " << type << " " << rhs;
}
-struct SubstitutionConstResult {
- // The resulting term of the substitution.
- Node term;
-
- // ?
- std::vector<Node> 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<Node>& sum, const std::vector<Node>& rep_sum,
- const std::map<Node, Node>& rep_to_const,
- const std::map<Node, Node>& rep_to_const_exp,
- const std::map<Node, Node>& rep_to_const_base) {
- Assert(sum.size() == rep_sum.size());
-
- SubstitutionConstResult result;
-
- std::vector<Node> vars;
- std::vector<Node> subs;
- std::set<Node> 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) {}
<< ", difference is " << mult_term << std::endl;
}
-class NonLinearExtentionSubstitutionSolver {
- public:
- NonLinearExtentionSubstitutionSolver(const eq::EqualityEngine* ee)
- : d_ee(ee) {}
-
- bool solve(const std::vector<Node>& vars, std::vector<Node>* subs,
- std::map<Node, std::vector<Node> >* exp,
- std::map<Node, std::vector<int> >* rep_to_subs_index);
-
- private:
- bool setSubstitutionConst(
- const std::vector<Node>& vars, Node r, Node r_c, Node r_cb,
- const std::vector<Node>& r_c_exp, std::vector<Node>* subs,
- std::map<Node, std::vector<Node> >* exp,
- std::map<Node, std::vector<int> >* rep_to_subs_index);
-
- const eq::EqualityEngine* d_ee;
-
- std::map<Node, Node > d_rep_sum_unique;
- std::map<Node, Node > d_rep_sum_unique_exp;
-
- std::map<Node, Node> d_rep_to_const;
- std::map<Node, Node> d_rep_to_const_exp;
- std::map<Node, Node> d_rep_to_const_base;
-
- // key in term_to_sum iff key in term_to_rep_sum.
- std::map<Node, std::vector<Node> > d_term_to_sum;
- std::map<Node, std::vector<Node> > d_term_to_rep_sum;
- std::map<Node, int> d_term_to_nconst_rep_count;
-
- std::map<Node, std::vector<Node> > d_reps_to_parent_terms;
- std::map<Node, std::vector<Node> > d_reps_to_terms;
-};
-
-bool NonLinearExtentionSubstitutionSolver::solve(
- const std::vector<Node>& vars, std::vector<Node>* subs,
- std::map<Node, std::vector<Node> >* exp,
- std::map<Node, std::vector<int> >* rep_to_subs_index) {
- // std::map<Node, Node> rep_to_const;
- // std::map<Node, Node> rep_to_const_exp;
- // std::map<Node, Node> rep_to_const_base;
-
- // std::map<Node, std::vector<Node> > term_to_sum;
- // std::map<Node, std::vector<Node> > term_to_rep_sum;
- // std::map<Node, int> term_to_nconst_rep_count;
- // std::map<Node, std::vector<Node> > reps_to_parent_terms;
- // std::map<Node, std::vector<Node> > 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<Node> 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<Node, Node> 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<Node, Node>::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<Node, Node>::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<Node>& vars, Node r, Node r_c, Node r_cb,
- const std::vector<Node>& r_c_exp, std::vector<Node>* subs,
- std::map<Node, std::vector<Node> >* exp,
- std::map<Node, std::vector<int> >* 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<Node, std::vector<int> >::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<Node>& 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<Node, Node> new_const;
- std::map<Node, std::vector<Node> > new_const_exp;
-
- // parent terms now evaluate to constants
- std::map<Node, std::vector<Node> >::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<Node>& 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<Node, std::vector<Node> >::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<Node, Node>::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<Node>& vars, std::vector<Node>& subs,
std::map<Node, std::vector<Node> >& exp) {
}
}
- 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;
projects / cvc5.git / commitdiff