From: Alex Ozdemir Date: Sun, 28 Jun 2020 12:51:31 +0000 (-0700) Subject: Proof Rules and Checker for Arithmetic (#4665) X-Git-Tag: cvc5-1.0.0~3170 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb68fa0f7b096bf086a7c7189e40805253ef1acf;p=cvc5.git 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. --- 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 >< 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 +#include + +#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& children, + const std::vector& 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 >< 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(); + 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(scalar)); + rightSum << nm->mkNode( + Kind::MULT, children[i][1], nm->mkConst(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 newBound = leastIntGreaterThan(originalBound); + auto nm = NodeManager::currentNM(); + Node rational = nm->mkConst(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 newBound = greatestIntLessThan(originalBound); + auto nm = NodeManager::currentNM(); + Node rational = nm->mkConst(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 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& children, + const std::vector& args) override; +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */