Reorganize candidate rewrite rule filtering (#2116)

1 files changed, 0 insertions, 372 deletions

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index e07f73540..ebd10c585 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -746,378 +746,6 @@ void SygusSampler::registerSygusType(TypeNode tn)
   }
 }
 
-SygusSamplerExt::SygusSamplerExt() : d_drewrite(nullptr), d_ssenm(*this) {}
-
-void SygusSamplerExt::initializeSygus(TermDbSygus* tds,
-                                      Node f,
-                                      unsigned nsamples,
-                                      bool useSygusType)
-{
-  SygusSampler::initializeSygus(tds, f, nsamples, useSygusType);
-  d_pairs.clear();
-  d_match_trie.clear();
-}
-
-void SygusSamplerExt::setDynamicRewriter(DynamicRewriter* dr)
-{
-  d_drewrite = dr;
-}
-
-Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
-{
-  Node eq_n = SygusSampler::registerTerm(n, forceKeep);
-  if (eq_n == n)
-  {
-    // this is a unique term
-    return n;
-  }
-  Node bn = n;
-  Node beq_n = eq_n;
-  if (d_use_sygus_type)
-  {
-    bn = d_tds->sygusToBuiltin(n);
-    beq_n = d_tds->sygusToBuiltin(eq_n);
-  }
-  Trace("sygus-synth-rr") << "sygusSampleExt : " << bn << "..." << beq_n
-                          << std::endl;
-  // whether we will keep this pair
-  bool keep = true;
-
-  // ----- check ordering redundancy
-  if (options::sygusRewSynthFilterOrder())
-  {
-    bool nor = isOrdered(bn);
-    bool eqor = isOrdered(beq_n);
-    Trace("sygus-synth-rr-debug") << "Ordered? : " << nor << " " << eqor
-                                  << std::endl;
-    if (eqor || nor)
-    {
-      // if only one is ordered, then we require that the ordered one's
-      // variables cannot be a strict subset of the variables of the other.
-      if (!eqor)
-      {
-        if (containsFreeVariables(beq_n, bn, true))
-        {
-          keep = false;
-        }
-        else
-        {
-          // if the previous value stored was unordered, but n is
-          // ordered, we prefer n. Thus, we force its addition to the
-          // sampler database.
-          SygusSampler::registerTerm(n, true);
-        }
-      }
-      else if (!nor)
-      {
-        keep = !containsFreeVariables(bn, beq_n, true);
-      }
-    }
-    else
-    {
-      keep = false;
-    }
-    if (!keep)
-    {
-      Trace("sygus-synth-rr") << "...redundant (unordered)" << std::endl;
-    }
-  }
-
-  // ----- check rewriting redundancy
-  if (keep && d_drewrite != nullptr)
-  {
-    Trace("sygus-synth-rr-debug") << "Check equal rewrite pair..." << std::endl;
-    if (d_drewrite->areEqual(bn, beq_n))
-    {
-      // must be unique according to the dynamic rewriter
-      Trace("sygus-synth-rr") << "...redundant (rewritable)" << std::endl;
-      keep = false;
-    }
-  }
-
-  if (options::sygusRewSynthFilterMatch())
-  {
-    // ----- check matchable
-    // check whether the pair is matchable with a previous one
-    d_curr_pair_rhs = beq_n;
-    Trace("sse-match") << "SSE check matches : " << bn << " [rhs = " << beq_n
-                       << "]..." << std::endl;
-    if (!d_match_trie.getMatches(bn, &d_ssenm))
-    {
-      keep = false;
-      Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl;
-      // regardless, would help to remember it
-      registerRelevantPair(n, eq_n);
-    }
-  }
-
-  if (keep)
-  {
-    return eq_n;
-  }
-  if (Trace.isOn("sygus-rr-filter"))
-  {
-    Printer* p = Printer::getPrinter(options::outputLanguage());
-    std::stringstream ss;
-    ss << "(redundant-rewrite ";
-    p->toStreamSygus(ss, n);
-    ss << " ";
-    p->toStreamSygus(ss, eq_n);
-    ss << ")";
-    Trace("sygus-rr-filter") << ss.str() << std::endl;
-  }
-  return Node::null();
-}
-
-void SygusSamplerExt::registerRelevantPair(Node n, Node eq_n)
-{
-  Node bn = n;
-  Node beq_n = eq_n;
-  if (d_use_sygus_type)
-  {
-    bn = d_tds->sygusToBuiltin(n);
-    beq_n = d_tds->sygusToBuiltin(eq_n);
-  }
-  // ----- check rewriting redundancy
-  if (d_drewrite != nullptr)
-  {
-    Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl;
-    Assert(!d_drewrite->areEqual(bn, beq_n));
-    d_drewrite->addRewrite(bn, beq_n);
-  }
-  if (options::sygusRewSynthFilterMatch())
-  {
-    // add to match information
-    for (unsigned r = 0; r < 2; r++)
-    {
-      Node t = r == 0 ? bn : beq_n;
-      Node to = r == 0 ? beq_n : bn;
-      // insert in match trie if first time
-      if (d_pairs.find(t) == d_pairs.end())
-      {
-        Trace("sse-match") << "SSE add term : " << t << std::endl;
-        d_match_trie.addTerm(t);
-      }
-      d_pairs[t].insert(to);
-    }
-  }
-}
-
-bool SygusSamplerExt::notify(Node s,
-                             Node n,
-                             std::vector<Node>& vars,
-                             std::vector<Node>& subs)
-{
-  Assert(!d_curr_pair_rhs.isNull());
-  std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
-      d_pairs.find(n);
-  if (Trace.isOn("sse-match"))
-  {
-    Trace("sse-match") << "  " << s << " matches " << n
-                       << " under:" << std::endl;
-    for (unsigned i = 0, size = vars.size(); i < size; i++)
-    {
-      Trace("sse-match") << "    " << vars[i] << " -> " << subs[i] << std::endl;
-      // TODO (#1923) ensure that we use an internal representation to
-      // ensure polymorphism is handled correctly
-      Assert(vars[i].getType().isComparableTo(subs[i].getType()));
-    }
-  }
-  Assert(it != d_pairs.end());
-  for (const Node& nr : it->second)
-  {
-    Node nrs =
-        nr.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
-    bool areEqual = (nrs == d_curr_pair_rhs);
-    if (!areEqual && d_drewrite != nullptr)
-    {
-      // if dynamic rewriter is available, consult it
-      areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
-    }
-    if (areEqual)
-    {
-      Trace("sse-match") << "*** Match, current pair: " << std::endl;
-      Trace("sse-match") << "  (" << s << ", " << d_curr_pair_rhs << ")"
-                         << std::endl;
-      Trace("sse-match") << "is an instance of previous pair:" << std::endl;
-      Trace("sse-match") << "  (" << n << ", " << nr << ")" << std::endl;
-      return false;
-    }
-  }
-  return true;
-}
-
-bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
-{
-  std::vector<Node> vars;
-  std::vector<Node> subs;
-  std::map<Node, Node> smap;
-
-  std::vector<std::vector<Node> > visit;
-  std::vector<MatchTrie*> visit_trie;
-  std::vector<int> visit_var_index;
-  std::vector<bool> visit_bound_var;
-
-  visit.push_back(std::vector<Node>{n});
-  visit_trie.push_back(this);
-  visit_var_index.push_back(-1);
-  visit_bound_var.push_back(false);
-  while (!visit.empty())
-  {
-    std::vector<Node> cvisit = visit.back();
-    MatchTrie* curr = visit_trie.back();
-    if (cvisit.empty())
-    {
-      Assert(n
-             == curr->d_data.substitute(
-                    vars.begin(), vars.end(), subs.begin(), subs.end()));
-      Trace("sse-match-debug") << "notify : " << curr->d_data << std::endl;
-      if (!ntm->notify(n, curr->d_data, vars, subs))
-      {
-        return false;
-      }
-      visit.pop_back();
-      visit_trie.pop_back();
-      visit_var_index.pop_back();
-      visit_bound_var.pop_back();
-    }
-    else
-    {
-      Node cn = cvisit.back();
-      Trace("sse-match-debug")
-          << "traverse : " << cn << " at depth " << visit.size() << std::endl;
-      unsigned index = visit.size() - 1;
-      int vindex = visit_var_index[index];
-      if (vindex == -1)
-      {
-        if (!cn.isVar())
-        {
-          Node op = cn.hasOperator() ? cn.getOperator() : cn;
-          unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
-          std::map<unsigned, MatchTrie>::iterator itu =
-              curr->d_children[op].find(nchild);
-          if (itu != curr->d_children[op].end())
-          {
-            // recurse on the operator or self
-            cvisit.pop_back();
-            if (cn.hasOperator())
-            {
-              for (const Node& cnc : cn)
-              {
-                cvisit.push_back(cnc);
-              }
-            }
-            Trace("sse-match-debug") << "recurse op : " << op << std::endl;
-            visit.push_back(cvisit);
-            visit_trie.push_back(&itu->second);
-            visit_var_index.push_back(-1);
-            visit_bound_var.push_back(false);
-          }
-        }
-        visit_var_index[index]++;
-      }
-      else
-      {
-        // clean up if we previously bound a variable
-        if (visit_bound_var[index])
-        {
-          Assert(!vars.empty());
-          smap.erase(vars.back());
-          vars.pop_back();
-          subs.pop_back();
-          visit_bound_var[index] = false;
-        }
-
-        if (vindex == static_cast<int>(curr->d_vars.size()))
-        {
-          Trace("sse-match-debug")
-              << "finished checking " << curr->d_vars.size()
-              << " variables at depth " << visit.size() << std::endl;
-          // finished
-          visit.pop_back();
-          visit_trie.pop_back();
-          visit_var_index.pop_back();
-          visit_bound_var.pop_back();
-        }
-        else
-        {
-          Trace("sse-match-debug") << "check variable #" << vindex
-                                   << " at depth " << visit.size() << std::endl;
-          Assert(vindex < static_cast<int>(curr->d_vars.size()));
-          // recurse on variable?
-          Node var = curr->d_vars[vindex];
-          bool recurse = true;
-          // check if it is already bound
-          std::map<Node, Node>::iterator its = smap.find(var);
-          if (its != smap.end())
-          {
-            if (its->second != cn)
-            {
-              recurse = false;
-            }
-          }
-          else
-          {
-            vars.push_back(var);
-            subs.push_back(cn);
-            smap[var] = cn;
-            visit_bound_var[index] = true;
-          }
-          if (recurse)
-          {
-            Trace("sse-match-debug") << "recurse var : " << var << std::endl;
-            cvisit.pop_back();
-            visit.push_back(cvisit);
-            visit_trie.push_back(&curr->d_children[var][0]);
-            visit_var_index.push_back(-1);
-            visit_bound_var.push_back(false);
-          }
-          visit_var_index[index]++;
-        }
-      }
-    }
-  }
-  return true;
-}
-
-void MatchTrie::addTerm(Node n)
-{
-  std::vector<Node> visit;
-  visit.push_back(n);
-  MatchTrie* curr = this;
-  while (!visit.empty())
-  {
-    Node cn = visit.back();
-    visit.pop_back();
-    if (cn.hasOperator())
-    {
-      curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
-      for (const Node& cnc : cn)
-      {
-        visit.push_back(cnc);
-      }
-    }
-    else
-    {
-      if (cn.isVar()
-          && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
-                 == curr->d_vars.end())
-      {
-        curr->d_vars.push_back(cn);
-      }
-      curr = &(curr->d_children[cn][0]);
-    }
-  }
-  curr->d_data = n;
-}
-
-void MatchTrie::clear()
-{
-  d_children.clear();
-  d_vars.clear();
-  d_data = Node::null();
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */