Remove quant EPR option (#5716)

This was an experimental option used in combination with separation logic.

1 files changed, 0 insertions, 187 deletions

diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp
deleted file mode 100644
index cf2deee11..000000000
--- a/src/theory/quantifiers/quant_epr.cpp
+++ /dev/null
@@ -1,187 +0,0 @@
-/*********************                                                        */
-/*! \file quant_epr.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of quantifier EPR.
- **/
-
-#include "theory/quantifiers/quant_epr.h"
-
-#include "theory/quantifiers/quant_util.h"
-
-using namespace CVC4::kind;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-void QuantEPR::registerNode(Node n,
-                            std::map<int, std::map<Node, bool> >& visited,
-                            bool beneathQuant,
-                            bool hasPol,
-                            bool pol)
-{
-  int vindex = hasPol ? (pol ? 1 : -1) : 0;
-  if (visited[vindex].find(n) == visited[vindex].end())
-  {
-    visited[vindex][n] = true;
-    Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl;
-    if (n.getKind() == FORALL)
-    {
-      if (beneathQuant || !hasPol || !pol)
-      {
-        for (unsigned i = 0; i < n[0].getNumChildren(); i++)
-        {
-          TypeNode tn = n[0][i].getType();
-          if (d_non_epr.find(tn) == d_non_epr.end())
-          {
-            Trace("quant-epr") << "Sort " << tn
-                               << " is non-EPR because of nested or possible "
-                                  "existential quantification."
-                               << std::endl;
-            d_non_epr[tn] = true;
-          }
-        }
-      }
-      else
-      {
-        beneathQuant = true;
-      }
-    }
-    TypeNode tn = n.getType();
-
-    if (n.getNumChildren() > 0)
-    {
-      if (tn.isSort())
-      {
-        if (d_non_epr.find(tn) == d_non_epr.end())
-        {
-          Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n
-                             << std::endl;
-          d_non_epr[tn] = true;
-        }
-      }
-      for (unsigned i = 0; i < n.getNumChildren(); i++)
-      {
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol);
-        registerNode(n[i], visited, beneathQuant, newHasPol, newPol);
-      }
-    }
-    else if (tn.isSort())
-    {
-      if (n.getKind() == BOUND_VARIABLE)
-      {
-        if (d_consts.find(tn) == d_consts.end())
-        {
-          // mark that at least one constant must occur
-          d_consts[tn].clear();
-        }
-      }
-      else if (std::find(d_consts[tn].begin(), d_consts[tn].end(), n)
-               == d_consts[tn].end())
-      {
-        d_consts[tn].push_back(n);
-        Trace("quant-epr") << "...constant of type " << tn << " : " << n
-                           << std::endl;
-      }
-    }
-  }
-}
-
-void QuantEPR::registerAssertion(Node assertion)
-{
-  std::map<int, std::map<Node, bool> > visited;
-  registerNode(assertion, visited, false, true, true);
-}
-
-void QuantEPR::finishInit()
-{
-  Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
-  for (std::map<TypeNode, std::vector<Node> >::iterator it = d_consts.begin();
-       it != d_consts.end();
-       ++it)
-  {
-    Assert(d_epr_axiom.find(it->first) == d_epr_axiom.end());
-    Trace("quant-epr-debug") << "process " << it->first << std::endl;
-    if (d_non_epr.find(it->first) != d_non_epr.end())
-    {
-      Trace("quant-epr-debug") << "...non-epr" << std::endl;
-      it->second.clear();
-    }
-    else
-    {
-      Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size()
-                               << std::endl;
-      if (it->second.empty())
-      {
-        it->second.push_back(NodeManager::currentNM()->mkSkolem(
-            "e", it->first, "EPR base constant"));
-      }
-      if (Trace.isOn("quant-epr"))
-      {
-        Trace("quant-epr") << "Type " << it->first
-                           << " is EPR, with constants : " << std::endl;
-        for (unsigned i = 0; i < it->second.size(); i++)
-        {
-          Trace("quant-epr") << "  " << it->second[i] << std::endl;
-        }
-      }
-    }
-  }
-}
-
-bool QuantEPR::isEPRConstant(TypeNode tn, Node k)
-{
-  return std::find(d_consts[tn].begin(), d_consts[tn].end(), k)
-         != d_consts[tn].end();
-}
-
-void QuantEPR::addEPRConstant(TypeNode tn, Node k)
-{
-  Assert(isEPR(tn));
-  Assert(d_epr_axiom.find(tn) == d_epr_axiom.end());
-  if (!isEPRConstant(tn, k))
-  {
-    d_consts[tn].push_back(k);
-  }
-}
-
-Node QuantEPR::mkEPRAxiom(TypeNode tn)
-{
-  Assert(isEPR(tn));
-  std::map<TypeNode, Node>::iterator ita = d_epr_axiom.find(tn);
-  if (ita == d_epr_axiom.end())
-  {
-    std::vector<Node> disj;
-    Node x = NodeManager::currentNM()->mkBoundVar(tn);
-    for (unsigned i = 0; i < d_consts[tn].size(); i++)
-    {
-      disj.push_back(
-          NodeManager::currentNM()->mkNode(EQUAL, x, d_consts[tn][i]));
-    }
-    Assert(!disj.empty());
-    d_epr_axiom[tn] = NodeManager::currentNM()->mkNode(
-        FORALL,
-        NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, x),
-        disj.size() == 1 ? disj[0]
-                         : NodeManager::currentNM()->mkNode(OR, disj));
-    return d_epr_axiom[tn];
-  }
-  else
-  {
-    return ita->second;
-  }
-}
-
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */