From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 31 Aug 2021 22:26:25 +0000 (-0700)
Subject: bv: Remove dump=bv-rewrites. (#7099)
X-Git-Tag: cvc5-1.0.0~1312
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e461f722ff0888165e63916ee4be8502bd0b657c;p=cvc5.git

bv: Remove dump=bv-rewrites. (#7099)

This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.
---

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 9dbbba7d3..630a91288 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -134,7 +134,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
       else if (!strcmp(optargPtr, "t-conflicts")
                || !strcmp(optargPtr, "t-lemmas")
                || !strcmp(optargPtr, "t-explanations")
-               || !strcmp(optargPtr, "bv-rewrites")
                || !strcmp(optargPtr, "theory::fullcheck"))
       {
       }
@@ -225,9 +224,6 @@ t-lemmas\n\
 t-explanations\n\
 + Output correctness queries for all theory explanations\n\
 \n\
-bv-rewrites\n\
-+ Output correctness queries for all bitvector rewrites\n\
-\n\
 theory::fullcheck\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 040d2c53f..fb80d43d0 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -445,32 +445,21 @@ public:
     SuppressWrongNoReturnWarning;
   }
 
-  template<bool checkApplies>
-  static inline Node run(TNode node) {
-    if (!checkApplies || applies(node)) {
-      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
+  template <bool checkApplies>
+  static inline Node run(TNode node)
+  {
+    if (!checkApplies || applies(node))
+    {
+      Debug("theory::bv::rewrite")
+          << "RewriteRule<" << rule << ">(" << node << ")" << std::endl;
       Assert(checkApplies || applies(node));
-      //++ s_statistics->d_ruleApplications;
       Node result = apply(node);
-      if (result != node) {
-        if(Dump.isOn("bv-rewrites")) {
-          std::ostringstream os;
-          os << "RewriteRule <"<<rule<<">; expect unsat";
-
-          Node condition = node.eqNode(result).notNode();
-
-          const Printer& printer =
-              smt::currentSmtEngine()->getOutputManager().getPrinter();
-          std::ostream& out =
-              smt::currentSmtEngine()->getOutputManager().getDumpOut();
-
-          printer.toStreamCmdComment(out, os.str());
-          printer.toStreamCmdCheckSat(out, condition);
-        }
-      }
-      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
+      Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node
+                                   << ") => " << result << std::endl;
       return result;
-    } else {
+    }
+    else
+    {
       return node;
     }
   }