From b35641f1a4ac8d70cf868b273971ee7c5e3b35f0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Jul 2021 13:55:13 -0500
Subject: [PATCH] Add arithmetic preprocess rewrite equality module (#6860)

This is the first part of a refactoring which will ensure that the linear arithmetic solver does not violate integer type constraints in its model.

This PR moves the method https://github.com/ajreynol/CVC4/blob/master/src/theory/arith/theory_arith.cpp#L129 to its own module / file.
---
 src/CMakeLists.txt                 |  2 +
 src/theory/arith/pp_rewrite_eq.cpp | 59 +++++++++++++++++++++++++++++
 src/theory/arith/pp_rewrite_eq.h   | 60 ++++++++++++++++++++++++++++++
 3 files changed, 121 insertions(+)
 create mode 100644 src/theory/arith/pp_rewrite_eq.cpp
 create mode 100644 src/theory/arith/pp_rewrite_eq.h

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 811f1c5ae..9fce77c80 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -467,6 +467,8 @@ libcvc5_add_sources(
   theory/arith/operator_elim.h
   theory/arith/partial_model.cpp
   theory/arith/partial_model.h
+  theory/arith/pp_rewrite_eq.cpp
+  theory/arith/pp_rewrite_eq.h
   theory/arith/proof_checker.cpp
   theory/arith/proof_checker.h
   theory/arith/proof_macros.h
diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp
new file mode 100644
index 000000000..45f972038
--- /dev/null
+++ b/src/theory/arith/pp_rewrite_eq.cpp
@@ -0,0 +1,59 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Preprocess equality rewriter for arithmetic
+ */
+
+#include "theory/arith/pp_rewrite_eq.h"
+
+#include "options/arith_options.h"
+#include "theory/rewriter.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+PreprocessRewriteEq::PreprocessRewriteEq(context::Context* c,
+                                         ProofNodeManager* pnm)
+    : d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_pnm(pnm)
+{
+}
+
+TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom)
+{
+  Assert(atom.getKind() == kind::EQUAL);
+  if (!options::arithRewriteEq())
+  {
+    return TrustNode::null();
+  }
+  Assert(atom[0].getType().isReal());
+  Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
+  Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
+  Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+  Debug("arith::preprocess")
+      << "arith::preprocess() : returning " << rewritten << std::endl;
+  // don't need to rewrite terms since rewritten is not a non-standard op
+  if (proofsEnabled())
+  {
+    return d_ppPfGen.mkTrustedRewrite(
+        atom,
+        rewritten,
+        d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+  }
+  return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
+}
+
+bool PreprocessRewriteEq::proofsEnabled() const { return d_pnm != nullptr; }
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/arith/pp_rewrite_eq.h b/src/theory/arith/pp_rewrite_eq.h
new file mode 100644
index 000000000..fc022f1d8
--- /dev/null
+++ b/src/theory/arith/pp_rewrite_eq.h
@@ -0,0 +1,60 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Preprocess equality rewriter for arithmetic
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__PP_REWRITE_EQ__H
+#define CVC5__THEORY__ARITH__PP_REWRITE_EQ__H
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "proof/eager_proof_generator.h"
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arith {
+
+/**
+ * This class is responsible for rewriting arithmetic equalities based on the
+ * current options.
+ *
+ * In particular, we may rewrite (= x y) to (and (>= x y) (<= x y)).
+ */
+class PreprocessRewriteEq
+{
+ public:
+  PreprocessRewriteEq(context::Context* c, ProofNodeManager* pnm);
+  ~PreprocessRewriteEq() {}
+  /**
+   * Preprocess equality, applies ppRewrite for equalities. This method is
+   * distinct from ppRewrite since it is not allowed to construct lemmas.
+   */
+  TrustNode ppRewriteEq(TNode eq);
+
+ private:
+  /** Are proofs enabled? */
+  bool proofsEnabled() const;
+  /** Used to prove pp-rewrites */
+  EagerProofGenerator d_ppPfGen;
+  /** Proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
-- 
2.30.2