Remove quantifiers rewrite rules infrastructure (#3754)

3 files changed, 0 insertions, 327 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 17d8cbed5..ce8d4fa88 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2841,251 +2841,4 @@ std::string DatatypeDeclarationCommand::getCommandName() const
   return "declare-datatypes";
 }
 
-/* -------------------------------------------------------------------------- */
-/* class RewriteRuleCommand                                                   */
-/* -------------------------------------------------------------------------- */
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
-                                       const std::vector<Expr>& guards,
-                                       Expr head,
-                                       Expr body,
-                                       const Triggers& triggers)
-    : d_vars(vars),
-      d_guards(guards),
-      d_head(head),
-      d_body(body),
-      d_triggers(triggers)
-{
-}
-
-RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
-                                       Expr head,
-                                       Expr body)
-    : d_vars(vars), d_head(head), d_body(body)
-{
-}
-
-const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; }
-const std::vector<Expr>& RewriteRuleCommand::getGuards() const
-{
-  return d_guards;
-}
-
-Expr RewriteRuleCommand::getHead() const { return d_head; }
-Expr RewriteRuleCommand::getBody() const { return d_body; }
-const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const
-{
-  return d_triggers;
-}
-
-void RewriteRuleCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    ExprManager* em = smtEngine->getExprManager();
-    /** build vars list */
-    Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
-    /** build guards list */
-    Expr guards;
-    if (d_guards.size() == 0)
-      guards = em->mkConst<bool>(true);
-    else if (d_guards.size() == 1)
-      guards = d_guards[0];
-    else
-      guards = em->mkExpr(kind::AND, d_guards);
-    /** build expression */
-    Expr expr;
-    if (d_triggers.empty())
-    {
-      expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body);
-    }
-    else
-    {
-      /** build triggers list */
-      std::vector<Expr> vtriggers;
-      vtriggers.reserve(d_triggers.size());
-      for (Triggers::const_iterator i = d_triggers.begin(),
-                                    end = d_triggers.end();
-           i != end;
-           ++i)
-      {
-        vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
-      }
-      Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
-      expr =
-          em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers);
-    }
-    smtEngine->assertFormula(expr);
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* RewriteRuleCommand::exportTo(ExprManager* exprManager,
-                                      ExprManagerMapCollection& variableMap)
-{
-  /** Convert variables */
-  VExpr vars = ExportTo(exprManager, variableMap, d_vars);
-  /** Convert guards */
-  VExpr guards = ExportTo(exprManager, variableMap, d_guards);
-  /** Convert triggers */
-  Triggers triggers;
-  triggers.reserve(d_triggers.size());
-  for (const std::vector<Expr>& trigger_list : d_triggers)
-  {
-    triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
-  }
-  /** Convert head and body */
-  Expr head = d_head.exportTo(exprManager, variableMap);
-  Expr body = d_body.exportTo(exprManager, variableMap);
-  /** Create the converted rules */
-  return new RewriteRuleCommand(vars, guards, head, body, triggers);
-}
-
-Command* RewriteRuleCommand::clone() const
-{
-  return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers);
-}
-
-std::string RewriteRuleCommand::getCommandName() const
-{
-  return "rewrite-rule";
-}
-
-/* -------------------------------------------------------------------------- */
-/* class PropagateRuleCommand                                                 */
-/* -------------------------------------------------------------------------- */
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
-                                           const std::vector<Expr>& guards,
-                                           const std::vector<Expr>& heads,
-                                           Expr body,
-                                           const Triggers& triggers,
-                                           bool deduction)
-    : d_vars(vars),
-      d_guards(guards),
-      d_heads(heads),
-      d_body(body),
-      d_triggers(triggers),
-      d_deduction(deduction)
-{
-}
-
-PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
-                                           const std::vector<Expr>& heads,
-                                           Expr body,
-                                           bool deduction)
-    : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction)
-{
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getVars() const
-{
-  return d_vars;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getGuards() const
-{
-  return d_guards;
-}
-
-const std::vector<Expr>& PropagateRuleCommand::getHeads() const
-{
-  return d_heads;
-}
-
-Expr PropagateRuleCommand::getBody() const { return d_body; }
-const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const
-{
-  return d_triggers;
-}
-
-bool PropagateRuleCommand::isDeduction() const { return d_deduction; }
-void PropagateRuleCommand::invoke(SmtEngine* smtEngine)
-{
-  try
-  {
-    ExprManager* em = smtEngine->getExprManager();
-    /** build vars list */
-    Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars);
-    /** build guards list */
-    Expr guards;
-    if (d_guards.size() == 0)
-      guards = em->mkConst<bool>(true);
-    else if (d_guards.size() == 1)
-      guards = d_guards[0];
-    else
-      guards = em->mkExpr(kind::AND, d_guards);
-    /** build heads list */
-    Expr heads;
-    if (d_heads.size() == 1)
-      heads = d_heads[0];
-    else
-      heads = em->mkExpr(kind::AND, d_heads);
-    /** build expression */
-    Expr expr;
-    if (d_triggers.empty())
-    {
-      expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body);
-    }
-    else
-    {
-      /** build triggers list */
-      std::vector<Expr> vtriggers;
-      vtriggers.reserve(d_triggers.size());
-      for (Triggers::const_iterator i = d_triggers.begin(),
-                                    end = d_triggers.end();
-           i != end;
-           ++i)
-      {
-        vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i));
-      }
-      Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers);
-      expr =
-          em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers);
-    }
-    smtEngine->assertFormula(expr);
-    d_commandStatus = CommandSuccess::instance();
-  }
-  catch (exception& e)
-  {
-    d_commandStatus = new CommandFailure(e.what());
-  }
-}
-
-Command* PropagateRuleCommand::exportTo(ExprManager* exprManager,
-                                        ExprManagerMapCollection& variableMap)
-{
-  /** Convert variables */
-  VExpr vars = ExportTo(exprManager, variableMap, d_vars);
-  /** Convert guards */
-  VExpr guards = ExportTo(exprManager, variableMap, d_guards);
-  /** Convert heads */
-  VExpr heads = ExportTo(exprManager, variableMap, d_heads);
-  /** Convert triggers */
-  Triggers triggers;
-  triggers.reserve(d_triggers.size());
-  for (const std::vector<Expr>& trigger_list : d_triggers)
-  {
-    triggers.push_back(ExportTo(exprManager, variableMap, trigger_list));
-  }
-  /** Convert head and body */
-  Expr body = d_body.exportTo(exprManager, variableMap);
-  /** Create the converted rules */
-  return new PropagateRuleCommand(vars, guards, heads, body, triggers);
-}
-
-Command* PropagateRuleCommand::clone() const
-{
-  return new PropagateRuleCommand(
-      d_vars, d_guards, d_heads, d_body, d_triggers);
-}
-
-std::string PropagateRuleCommand::getCommandName() const
-{
-  return "propagate-rule";
-}
 }  // namespace CVC4
diff --git a/src/smt/command.h b/src/smt/command.h
index d82399135..19b858bd6 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1315,80 +1315,6 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
   std::string getCommandName() const override;
 }; /* class DatatypeDeclarationCommand */
 
-class CVC4_PUBLIC RewriteRuleCommand : public Command
-{
- public:
-  typedef std::vector<std::vector<Expr> > Triggers;
-
- protected:
-  typedef std::vector<Expr> VExpr;
-  VExpr d_vars;
-  VExpr d_guards;
-  Expr d_head;
-  Expr d_body;
-  Triggers d_triggers;
-
- public:
-  RewriteRuleCommand(const std::vector<Expr>& vars,
-                     const std::vector<Expr>& guards,
-                     Expr head,
-                     Expr body,
-                     const Triggers& d_triggers);
-  RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body);
-
-  const std::vector<Expr>& getVars() const;
-  const std::vector<Expr>& getGuards() const;
-  Expr getHead() const;
-  Expr getBody() const;
-  const Triggers& getTriggers() const;
-
-  void invoke(SmtEngine* smtEngine) override;
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-}; /* class RewriteRuleCommand */
-
-class CVC4_PUBLIC PropagateRuleCommand : public Command
-{
- public:
-  typedef std::vector<std::vector<Expr> > Triggers;
-
- protected:
-  typedef std::vector<Expr> VExpr;
-  VExpr d_vars;
-  VExpr d_guards;
-  VExpr d_heads;
-  Expr d_body;
-  Triggers d_triggers;
-  bool d_deduction;
-
- public:
-  PropagateRuleCommand(const std::vector<Expr>& vars,
-                       const std::vector<Expr>& guards,
-                       const std::vector<Expr>& heads,
-                       Expr body,
-                       const Triggers& d_triggers,
-                       /* true if we want a deduction rule */
-                       bool d_deduction = false);
-  PropagateRuleCommand(const std::vector<Expr>& vars,
-                       const std::vector<Expr>& heads,
-                       Expr body,
-                       bool d_deduction = false);
-
-  const std::vector<Expr>& getVars() const;
-  const std::vector<Expr>& getGuards() const;
-  const std::vector<Expr>& getHeads() const;
-  Expr getBody() const;
-  const Triggers& getTriggers() const;
-  bool isDeduction() const;
-  void invoke(SmtEngine* smtEngine) override;
-  Command* exportTo(ExprManager* exprManager,
-                    ExprManagerMapCollection& variableMap) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-}; /* class PropagateRuleCommand */
-
 class CVC4_PUBLIC ResetCommand : public Command
 {
  public:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ad4d4e1d5..1d96fc207 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3630,12 +3630,6 @@ void SmtEnginePrivate::addFormula(
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());
     }
-    // rewrite rules are by default in the unsat core because
-    // they need to be applied until saturation
-    if(options::unsatCores() &&
-       n.getKind() == kind::REWRITE_RULE ){
-      ProofManager::currentPM()->addUnsatCore(n.toExpr());
-    }
   );
 
   // Add the normalized formula to the queue