diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-09-28 20:14:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-28 22:14:47 -0500 |
commit | b830fb6747b5a5304100217e91481d9cc6c4f1c5 (patch) | |
tree | 543bec0e587e5e9e81a3f4620ffa9f6864b69d90 | |
parent | a6ce4fb305e95d8956dcb2bdb57d801b8d092206 (diff) |
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.
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.cpp | 34 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 7 |
3 files changed, 43 insertions, 0 deletions
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 */ |