Remove nl solve subs option. (#1803)

2 files changed, 0 insertions, 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
@@ -478,15 +478,6 @@ header = "options/arith_options.h"
   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"
   long       = "nl-ext-purify"
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<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) {
@@ -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<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) {}
@@ -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<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) {
@@ -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;