Remove quantifiers rewrite rules infrastructure (#3754)

1 files changed, 0 insertions, 27 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3ab3c0eb1..9800cbe91 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -626,33 +626,6 @@ void Smt2::resetAssertions() {
   }
 }
 
-std::unique_ptr<Command> Smt2::assertRewriteRule(
-    Kind kind,
-    Expr bvl,
-    const std::vector<Expr>& triggers,
-    const std::vector<Expr>& guards,
-    const std::vector<Expr>& heads,
-    Expr body)
-{
-  assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION
-         || kind == kind::RR_DEDUCTION);
-
-  ExprManager* em = getExprManager();
-
-  std::vector<Expr> args;
-  args.push_back(mkAnd(heads));
-  args.push_back(body);
-
-  if (!triggers.empty())
-  {
-    args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers));
-  }
-
-  Expr rhs = em->mkExpr(kind, args);
-  Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs);
-  return std::unique_ptr<Command>(new AssertCommand(rule, false));
-}
-
 Smt2::SynthFunFactory::SynthFunFactory(
     Smt2* smt2,
     const std::string& fun,