From b830fb6747b5a5304100217e91481d9cc6c4f1c5 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 28 Sep 2020 20:14:47 -0700
Subject: [PATCH] Add utilities for arith/proof_checker and build it (#5157)

The arith proof checker was not being built (not in cmake). Now it is. A
few dependencies were missing.
---
 src/CMakeLists.txt                   |  2 ++
 src/theory/arith/arith_utilities.cpp | 34 ++++++++++++++++++++++++++++
 src/theory/arith/arith_utilities.h   |  7 ++++++
 3 files changed, 43 insertions(+)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 620bcc352..587f845d3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -371,6 +371,8 @@ libcvc4_add_sources(
   theory/arith/operator_elim.h
   theory/arith/partial_model.cpp
   theory/arith/partial_model.h
+  theory/arith/proof_checker.cpp
+  theory/arith/proof_checker.h
   theory/arith/simplex.cpp
   theory/arith/simplex.h
   theory/arith/simplex_update.cpp
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index f07c31141..cbd976b03 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -278,6 +278,40 @@ Node mkBounded(Node l, Node a, Node u)
   return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
 }
 
+Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
+
+Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
+
+Node negateProofLiteral(TNode n)
+{
+  auto nm = NodeManager::currentNM();
+  switch (n.getKind())
+  {
+    case Kind::GT:
+    {
+      return nm->mkNode(Kind::LEQ, n[0], n[1]);
+    }
+    case Kind::LT:
+    {
+      return nm->mkNode(Kind::GEQ, n[0], n[1]);
+    }
+    case Kind::LEQ:
+    {
+      return nm->mkNode(Kind::GT, n[0], n[1]);
+    }
+    case Kind::GEQ:
+    {
+      return nm->mkNode(Kind::LT, n[0], n[1]);
+    }
+    case Kind::EQUAL:
+    case Kind::NOT:
+    {
+      return n.negate();
+    }
+    default: Unhandled() << n;
+  }
+}
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index a64208330..9e421efc7 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -338,6 +338,13 @@ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs);
 /** Make the node u >= a ^ a >= l */
 Node mkBounded(Node l, Node a, Node u);
 
+Rational leastIntGreaterThan(const Rational&);
+
+Rational greatestIntLessThan(const Rational&);
+
+/** Negates a node in arithmetic proof normal form. */
+Node negateProofLiteral(TNode n);
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-- 
2.30.2