Proof Rules and Checker for Arithmetic (#4665)

This PR introduces proof rules for arithmetic and their checker.

The code is dead, since these rules are never used.

4 files changed, 389 insertions, 0 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index f736efed9..d00f1658b 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -90,6 +90,13 @@ const char* toString(PfRule id)
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
     case PfRule::INSTANTIATE: return "INSTANTIATE";
+    //================================================= Arith rules
+    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS";
+    case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
+    case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
+    case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
+    case PfRule::INT_TRUST: return "INT_TRUST";
+    case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index d6e5b6f4b..ec589a16e 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -507,6 +507,70 @@ enum class PfRule : uint32_t
   // sigma maps x1 ... xn to t1 ... tn.
   INSTANTIATE,
 
+  // ======== Adding Inequalities
+  // Note: an ArithLiteral is a term of the form (>< poly const)
+  // where
+  //   >< is >=, >, ==, <, <=, or not(== ...).
+  //   poly is a polynomial
+  //   const is a rational constant
+
+  // Children: (P1:l1, ..., Pn:ln)
+  //           where each li is an ArithLiteral
+  //           not(= ...) is dis-allowed!
+  //
+  // Arguments: (k1, ..., kn), non-zero reals
+  // ---------------------
+  // Conclusion: (>< (* k t1) (* k t2))
+  //    where >< is the fusion of the combination of the ><i, (flipping each it
+  //    its ki is negative). >< is always one of <, <=
+  //    NB: this implies that lower bounds must have negative ki,
+  //                      and upper bounds must have positive ki.
+  //    t1 is the sum of the polynomials.
+  //    t2 is the sum of the constants.
+  ARITH_SCALE_SUM_UPPER_BOUNDS,
+
+  // ======== Tightening Strict Integer Upper Bounds
+  // Children: (P:(< i c))
+  //         where i has integer type.
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (<= i greatestIntLessThan(c)})
+  INT_TIGHT_UB,
+
+  // ======== Tightening Strict Integer Lower Bounds
+  // Children: (P:(> i c))
+  //         where i has integer type.
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (>= i leastIntGreaterThan(c)})
+  INT_TIGHT_LB,
+
+  // ======== Trichotomy of the reals
+  // Children: (A B)
+  // Arguments: (C)
+  // ---------------------
+  // Conclusion: (C),
+  //                 where (not A) (not B) and C
+  //                   are (> x c) (< x c) and (= x c)
+  //                   in some order
+  //                 note that "not" here denotes arithmetic negation, flipping
+  //                 >= to <, etc.
+  ARITH_TRICHOTOMY,
+
+  // ======== Arithmetic operator elimination
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: arith::OperatorElim::getAxiomFor(t)
+  ARITH_OP_ELIM_AXIOM,
+
+  // ======== Int Trust
+  // Children: (P1 ... Pn)
+  // Arguments: (Q)
+  // ---------------------
+  // Conclusion: (Q)
+  INT_TRUST,
+
   //================================================= Unknown rule
   UNKNOWN,
 };
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
new file mode 100644
index 000000000..5b7a3d63a
--- /dev/null
+++ b/src/theory/arith/proof_checker.cpp
@@ -0,0 +1,269 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Implementation of arithmetic proof checker
+ **/
+
+#include "theory/arith/proof_checker.h"
+
+#include <iostream>
+#include <set>
+
+#include "expr/skolem_manager.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/constraint.h"
+#include "theory/arith/normal_form.h"
+#include "theory/arith/operator_elim.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+void ArithProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  pc->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, this);
+  pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this);
+  pc->registerChecker(PfRule::INT_TIGHT_UB, this);
+  pc->registerChecker(PfRule::INT_TIGHT_LB, this);
+  pc->registerChecker(PfRule::INT_TRUST, this);
+  pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
+}
+
+Node ArithProofRuleChecker::checkInternal(PfRule id,
+                                          const std::vector<Node>& children,
+                                          const std::vector<Node>& args)
+{
+  if (Debug.isOn("arith::pf::check"))
+  {
+    Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl;
+    Debug("arith::pf::check") << "  children: " << std::endl;
+    for (const auto& c : children)
+    {
+      Debug("arith::pf::check") << "  * " << c << std::endl;
+    }
+    Debug("arith::pf::check") << "  args:" << std::endl;
+    for (const auto& c : args)
+    {
+      Debug("arith::pf::check") << "  * " << c << std::endl;
+    }
+  }
+  switch (id)
+  {
+    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS:
+    {
+      // Children: (P1:l1, ..., Pn:ln)
+      //           where each li is an ArithLiteral
+      //           not(= ...) is dis-allowed!
+      //
+      // Arguments: (k1, ..., kn), non-zero reals
+      // ---------------------
+      // Conclusion: (>< (* k t1) (* k t2))
+      //    where >< is the fusion of the combination of the ><i, (flipping each
+      //    it its ki is negative). >< is always one of <, <= NB: this implies
+      //    that lower bounds must have negative ki,
+      //                      and upper bounds must have positive ki.
+      //    t1 is the sum of the polynomials.
+      //    t2 is the sum of the constants.
+      Assert(children.size() == args.size());
+      if (children.size() < 2)
+      {
+        return Node::null();
+      }
+
+      // Whether a strict inequality is in the sum.
+      auto nm = NodeManager::currentNM();
+      bool strict = false;
+      NodeBuilder<> leftSum(Kind::PLUS);
+      NodeBuilder<> rightSum(Kind::PLUS);
+      for (size_t i = 0; i < children.size(); ++i)
+      {
+        Rational scalar = args[i].getConst<Rational>();
+        if (scalar == 0)
+        {
+          Debug("arith::pf::check") << "Error: zero scalar" << std::endl;
+          return Node::null();
+        }
+
+        // Adjust strictness
+        switch (children[i].getKind())
+        {
+          case Kind::GT:
+          case Kind::LT:
+          {
+            strict = true;
+            break;
+          }
+          case Kind::GEQ:
+          case Kind::LEQ:
+          case Kind::EQUAL:
+          {
+            break;
+          }
+          default:
+          {
+            Debug("arith::pf::check")
+                << "Bad kind: " << children[i].getKind() << std::endl;
+          }
+        }
+        // Check sign
+        switch (children[i].getKind())
+        {
+          case Kind::GT:
+          case Kind::GEQ:
+          {
+            if (scalar > 0)
+            {
+              Debug("arith::pf::check")
+                  << "Positive scalar for lower bound: " << scalar << " for "
+                  << children[i] << std::endl;
+              return Node::null();
+            }
+            break;
+          }
+          case Kind::LEQ:
+          case Kind::LT:
+          {
+            if (scalar < 0)
+            {
+              Debug("arith::pf::check")
+                  << "Negative scalar for upper bound: " << scalar << " for "
+                  << children[i] << std::endl;
+              return Node::null();
+            }
+            break;
+          }
+          case Kind::EQUAL:
+          {
+            break;
+          }
+          default:
+          {
+            Debug("arith::pf::check")
+                << "Bad kind: " << children[i].getKind() << std::endl;
+          }
+        }
+        leftSum << nm->mkNode(
+            Kind::MULT, children[i][0], nm->mkConst<Rational>(scalar));
+        rightSum << nm->mkNode(
+            Kind::MULT, children[i][1], nm->mkConst<Rational>(scalar));
+      }
+      Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
+                          leftSum.constructNode(),
+                          rightSum.constructNode());
+      return r;
+    }
+    case PfRule::INT_TIGHT_LB:
+    {
+      // Children: (P:(> i c))
+      //         where i has integer type.
+      // Arguments: none
+      // ---------------------
+      // Conclusion: (>= i leastIntGreaterThan(c)})
+      if (children.size() != 1
+          || (children[0].getKind() != Kind::GT
+              && children[0].getKind() != Kind::GEQ)
+          || !children[0][0].getType().isInteger()
+          || children[0][1].getKind() != Kind::CONST_RATIONAL)
+      {
+        Debug("arith::pf::check") << "Illformed input: " << children;
+        return Node::null();
+      }
+      else
+      {
+        Rational originalBound = children[0][1].getConst<Rational>();
+        Rational newBound = leastIntGreaterThan(originalBound);
+        auto nm = NodeManager::currentNM();
+        Node rational = nm->mkConst<Rational>(newBound);
+        return nm->mkNode(kind::GEQ, children[0][0], rational);
+      }
+    }
+    case PfRule::INT_TIGHT_UB:
+    {
+      // ======== Tightening Strict Integer Upper Bounds
+      // Children: (P:(< i c))
+      //         where i has integer type.
+      // Arguments: none
+      // ---------------------
+      // Conclusion: (<= i greatestIntLessThan(c)})
+      if (children.size() != 1
+          || (children[0].getKind() != Kind::LT
+              && children[0].getKind() != Kind::LEQ)
+          || !children[0][0].getType().isInteger()
+          || children[0][1].getKind() != Kind::CONST_RATIONAL)
+      {
+        Debug("arith::pf::check") << "Illformed input: " << children;
+        return Node::null();
+      }
+      else
+      {
+        Rational originalBound = children[0][1].getConst<Rational>();
+        Rational newBound = greatestIntLessThan(originalBound);
+        auto nm = NodeManager::currentNM();
+        Node rational = nm->mkConst<Rational>(newBound);
+        return nm->mkNode(kind::LEQ, children[0][0], rational);
+      }
+    }
+    case PfRule::ARITH_TRICHOTOMY:
+    {
+      Node a = negateProofLiteral(children[0]);
+      Node b = negateProofLiteral(children[1]);
+      Node c = args[0];
+      if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1])
+      {
+        std::set<Kind> cmps;
+        cmps.insert(a.getKind());
+        cmps.insert(b.getKind());
+        cmps.insert(c.getKind());
+        if (cmps.count(Kind::EQUAL) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No = " << std::endl;
+          return Node::null();
+        }
+        if (cmps.count(Kind::GT) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No > " << std::endl;
+          return Node::null();
+        }
+        if (cmps.count(Kind::LT) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No < " << std::endl;
+          return Node::null();
+        }
+        return args[0];
+      }
+      else
+      {
+        Debug("arith::pf::check")
+            << "Error: Different polynomials / values" << std::endl;
+        Debug("arith::pf::check") << "  a: " << a << std::endl;
+        Debug("arith::pf::check") << "  b: " << b << std::endl;
+        Debug("arith::pf::check") << "  c: " << c << std::endl;
+        return Node::null();
+      }
+      // Check that all have the same constant:
+    }
+    case PfRule::INT_TRUST:
+    {
+      Assert(args.size() == 1);
+      return args[0];
+    }
+    case PfRule::ARITH_OP_ELIM_AXIOM:
+    {
+      Assert(children.empty());
+      Assert(args.size() == 1);
+      return OperatorElim::getAxiomFor(args[0]);
+    }
+    default: return Node::null();
+  }
+}
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
new file mode 100644
index 000000000..b8a5d0df7
--- /dev/null
+++ b/src/theory/arith/proof_checker.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Arithmetic proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__PROOF_CHECKER_H
+#define CVC4__THEORY__ARITH__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/** A checker for arithmetic reasoning in proofs */
+class ArithProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  ArithProofRuleChecker() {}
+  ~ArithProofRuleChecker() {}
+
+  /** Register all rules owned by this rule checker into pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */