Remove --apply-to-const preprocessing pass (#3919)

Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.

6 files changed, 0 insertions, 177 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index aaa789308..57f0ec95e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -42,8 +42,6 @@ libcvc4_add_sources(
   preprocessing/passes/ackermann.h
   preprocessing/passes/apply_substs.cpp
   preprocessing/passes/apply_substs.h
-  preprocessing/passes/apply_to_const.cpp
-  preprocessing/passes/apply_to_const.h
   preprocessing/passes/bool_to_bv.cpp
   preprocessing/passes/bool_to_bv.h
   preprocessing/passes/bv_abstraction.cpp
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 88842faf7..676e01484 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -634,15 +634,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "amount of resources spent for each sat conflict (bitvectors)"
 
-[[option]]
-  name       = "rewriteApplyToConst"
-  category   = "expert"
-  long       = "rewrite-apply-to-const"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "eliminate function applications, rewriting e.g. f(5) to a new symbol f_5"
-
 # --replay is currently broken; don't document it for 1.0
 [[option]]
   name       = "replayInputFilename"
diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp
deleted file mode 100644
index e8681e40c..000000000
--- a/src/preprocessing/passes/apply_to_const.cpp
+++ /dev/null
@@ -1,108 +0,0 @@
-/*********************                                                        */
-/*! \file apply_to_const.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Haniel Barbosa, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 The ApplyToConst preprocessing pass
- **
- ** Rewrites applies to constants
- **/
-
-#include "preprocessing/passes/apply_to_const.h"
-
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-namespace preprocessing {
-namespace passes {
-
-using namespace CVC4::theory;
-
-ApplyToConst::ApplyToConst(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "apply-to-const"){};
-
-Node ApplyToConst::rewriteApplyToConst(TNode n, NodeMap& cache)
-{
-  Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
-
-  if (n.getMetaKind() == kind::metakind::CONSTANT
-      || n.getMetaKind() == kind::metakind::VARIABLE
-      || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR)
-  {
-    return n;
-  }
-
-  if (cache.find(n) != cache.end())
-  {
-    Trace("rewriteApplyToConst") << "in cache :: " << cache[n] << std::endl;
-    return cache[n];
-  }
-
-  if (n.getKind() == kind::APPLY_UF)
-  {
-    if (n.getNumChildren() == 1 && n[0].isConst() && n[0].getType().isInteger())
-    {
-      stringstream ss;
-      ss << n.getOperator() << "_";
-      if (n[0].getConst<Rational>() < 0)
-      {
-        ss << "m" << -n[0].getConst<Rational>();
-      }
-      else
-      {
-        ss << n[0];
-      }
-      Node newvar =
-          NodeManager::currentNM()->mkSkolem(ss.str(),
-                                             n.getType(),
-                                             "rewriteApplyToConst skolem",
-                                             NodeManager::SKOLEM_EXACT_NAME);
-      cache[n] = newvar;
-      Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
-      return newvar;
-    }
-    Unhandled()
-        << "The rewrite-apply-to-const preprocessor is currently limited;\n"
-        << "it only works if all function symbols are unary and with Integer\n"
-        << "domain, and all applications are to integer values.\n"
-        << "Found application: " << n;
-  }
-
-  NodeBuilder<> builder(n.getKind());
-  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
-  {
-    builder << n.getOperator();
-  }
-  for (unsigned i = 0; i < n.getNumChildren(); ++i)
-  {
-    builder << rewriteApplyToConst(n[i], cache);
-  }
-  Node rewr = builder;
-  cache[n] = rewr;
-  Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl;
-  return rewr;
-}
-
-PreprocessingPassResult ApplyToConst::applyInternal(
-    AssertionPipeline* assertionsToPreprocess)
-{
-  NodeMap cache;
-  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
-  {
-    assertionsToPreprocess->replace(i,
-                                    Rewriter::rewrite(rewriteApplyToConst(
-                                        (*assertionsToPreprocess)[i], cache)));
-  }
-  return PreprocessingPassResult::NO_CONFLICT;
-}
-
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace CVC4
diff --git a/src/preprocessing/passes/apply_to_const.h b/src/preprocessing/passes/apply_to_const.h
deleted file mode 100644
index 4c1df22ca..000000000
--- a/src/preprocessing/passes/apply_to_const.h
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/*! \file apply_to_const.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Haniel Barbosa
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 The ApplyToConst preprocessing pass
- **
- ** Rewrites applies to constants
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
-#define CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
-
-#include <unordered_map>
-
-#include "expr/node.h"
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-
-namespace CVC4 {
-namespace preprocessing {
-namespace passes {
-
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
-
-class ApplyToConst : public PreprocessingPass
-{
- public:
-  ApplyToConst(PreprocessingPassContext* preprocContext);
-
- protected:
-  PreprocessingPassResult applyInternal(
-      AssertionPipeline* assertionsToPreprocess) override;
-
- private:
-  Node rewriteApplyToConst(TNode n, NodeMap& cache);
-};
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace CVC4
-
-#endif /* CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 154ed9086..9272bbb5a 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -25,7 +25,6 @@
 #include "base/output.h"
 #include "preprocessing/passes/ackermann.h"
 #include "preprocessing/passes/apply_substs.h"
-#include "preprocessing/passes/apply_to_const.h"
 #include "preprocessing/passes/bool_to_bv.h"
 #include "preprocessing/passes/bv_abstraction.h"
 #include "preprocessing/passes/bv_eager_atoms.h"
@@ -122,7 +121,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("bv-gauss", callCtor<BVGauss>);
   registerPassInfo("static-learning", callCtor<StaticLearning>);
   registerPassInfo("ite-simp", callCtor<ITESimp>);
-  registerPassInfo("apply-to-const", callCtor<ApplyToConst>);
   registerPassInfo("global-negate", callCtor<GlobalNegate>);
   registerPassInfo("int-to-bv", callCtor<IntToBV>);
   registerPassInfo("bv-to-int", callCtor<BVToInt>);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 89f3acd56..43459dcec 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3557,11 +3557,6 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-repeat-simplify", d_assertions);
 
-  if (options::rewriteApplyToConst())
-  {
-    d_passes["apply-to-const"]->apply(&d_assertions);
-  }
-
   if (options::ufHo())
   {
     d_passes["ho-elim"]->apply(&d_assertions);