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.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 620bcc3528c054f9bc9a71e1b43ae3b09f8f347f..587f845d3f958bdc6727a3c6074c8a164a82fbf1 100644 (file)
--- 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 f07c31141b70b77145028d2424902f2000004ff7..cbd976b032e5498d8c561e5570e65dca4cdfd6dd 100644 (file)
--- 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 a6420833030561b6b61aacccecb15da67c1d8010..9e421efc7f4a0904b53acbfad66dbef84a487db6 100644 (file)
--- 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 */