This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
theory/arith/nl/cad/constraints.h
theory/arith/nl/cad/projections.cpp
theory/arith/nl/cad/projections.h
+ theory/arith/nl/cad/proof_checker.cpp
+ theory/arith/nl/cad/proof_checker.h
+ theory/arith/nl/cad/proof_generator.cpp
+ theory/arith/nl/cad/proof_generator.h
theory/arith/nl/cad/variable_ordering.cpp
theory/arith/nl/cad/variable_ordering.h
theory/arith/nl/ext/constraint.cpp
return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
+ case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
+ case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
default: return "?";
// secant of p from l to u.
ARITH_TRANS_SINE_APPROX_BELOW_POS,
+ // ================ CAD Lemmas
+ // We use IRP for IndexedRootPredicate.
+ //
+ // A formula "Interval" describes that a variable (xn is none is given) is
+ // within a particular interval whose bounds are given as IRPs. It is either
+ // an open interval or a point interval:
+ // (IRP k poly) < xn < (IRP k poly)
+ // xn == (IRP k poly)
+ //
+ // A formula "Cell" describes a portion
+ // of the real space in the following form:
+ // Interval(x1) and Interval(x2) and ...
+ // We implicitly assume a Cell to go up to n-1 (and can be empty).
+ //
+ // A formula "Covering" is a set of Intervals, implying that xn can be in
+ // neither of these intervals. To be a covering (of the real line), the union
+ // of these intervals should be the real numbers.
+ // ======== CAD direct conflict
+ // Children (Cell, A)
+ // ---------------------
+ // Conclusion: (false)
+ // A direct interval is generated from an assumption A (in variables x1...xn)
+ // over a Cell (in variables x1...xn). It derives that A evaluates to false
+ // over the Cell. In the actual algorithm, it means that xn can not be in the
+ // topmost interval of the Cell.
+ ARITH_NL_CAD_DIRECT,
+ // ======== CAD recursive interval
+ // Children (Cell, Covering)
+ // ---------------------
+ // Conclusion: (false)
+ // A recursive interval is generated from a Covering (for xn) over a Cell
+ // (in variables x1...xn-1). It generates the conclusion that no xn exists
+ // that extends the Cell and satisfies all assumptions.
+ ARITH_NL_CAD_RECURSIVE,
+
//================================================= Unknown rule
UNKNOWN,
};
--- /dev/null
+/********************* */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 CAD proof checker
+ **/
+
+#include "theory/arith/nl/cad/proof_checker.h"
+
+#include "expr/sequence.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+void CADProofRuleChecker::registerTo(ProofChecker* pc)
+{
+ // trusted rules
+ pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_DIRECT, this, 2);
+ pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_RECURSIVE, this, 2);
+}
+
+Node CADProofRuleChecker::checkInternal(PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ Trace("nl-cad-checker") << "Checking " << id << std::endl;
+ for (const auto& c : children)
+ {
+ Trace("nl-cad-checker") << "\t" << c << std::endl;
+ }
+ if (id == PfRule::ARITH_NL_CAD_DIRECT)
+ {
+ Assert(args.size() == 1);
+ return args[0];
+ }
+ if (id == PfRule::ARITH_NL_CAD_RECURSIVE)
+ {
+ Assert(args.size() == 1);
+ return args[0];
+ }
+ return Node::null();
+}
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 CAD proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#define CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * A checker for CAD proofs
+ *
+ * This proof checker takes care of the two CAD proof rules ARITH_NL_CAD_DIRECT
+ * and ARITH_NL_CAD_RECURSIVE. It does not do any actual proof checking yet, but
+ * considers them to be trusted rules.
+ */
+class CADProofRuleChecker : public ProofRuleChecker
+{
+ public:
+ CADProofRuleChecker() {}
+ ~CADProofRuleChecker() {}
+
+ /** Register all rules owned by this rule checker in 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 cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
--- /dev/null
+/********************* */
+/*! \file proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 CAD proof generator
+ **/
+
+#include "theory/arith/nl/cad/proof_generator.h"
+
+#ifdef CVC4_POLY_IMP
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+namespace {
+/**
+ * Retrieves the root indices of the sign-invariant region of v.
+ *
+ * We assume that roots holds a sorted list of roots from one polynomial.
+ * If v is equal to one of these roots, we return (id,id) where id is the index
+ * of this root within roots. Otherwise, we return the id of the largest root
+ * below v and the id of the smallest root above v. To make sure a smaller root
+ * and a larger root always exist, we implicitly extend the roots by -infty and
+ * infty.
+ *
+ * ATTENTION: if we return id, the corresponding root is:
+ * - id = 0: -infty
+ * - 0 < id <= roots.size(): roots[id-1]
+ * - id = roots.size() + 1: infty
+ */
+std::pair<std::size_t, std::size_t> getRootIDs(
+ const std::vector<poly::Value>& roots, const poly::Value& v)
+{
+ for (std::size_t i = 0; i < roots.size(); ++i)
+ {
+ if (roots[i] == v)
+ {
+ return {i + 1, i + 1};
+ }
+ if (roots[i] > v)
+ {
+ return {i, i + 1};
+ }
+ }
+ return {roots.size(), roots.size() + 1};
+}
+
+/**
+ * Constructs an IndexedRootExpression:
+ * var ~rel~ root_k(poly)
+ * where root_k(poly) is "the k'th root of the polynomial".
+ *
+ * @param var The variable that is bounded
+ * @param rel The relation for this constraint
+ * @param zero A node representing Rational(0)
+ * @param k The index of the root (starting with 1)
+ * @param poly The polynomial whose root shall be considered
+ * @param vm A variable mapper from CVC4 to libpoly variables
+ */
+Node mkIRP(const Node& var,
+ Kind rel,
+ const Node& zero,
+ std::size_t k,
+ const poly::Polynomial& poly,
+ VariableMapper& vm)
+{
+ auto* nm = NodeManager::currentNM();
+ auto op = nm->mkConst<IndexedRootPredicate>(IndexedRootPredicate(k));
+ return nm->mkNode(Kind::INDEXED_ROOT_PREDICATE,
+ op,
+ nm->mkNode(rel, var, zero),
+ as_cvc_polynomial(poly, vm));
+}
+
+} // namespace
+
+CADProofGenerator::CADProofGenerator(context::Context* ctx,
+ ProofNodeManager* pnm)
+ : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
+{
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+ d_zero = NodeManager::currentNM()->mkConst<Rational>(0);
+}
+
+void CADProofGenerator::startNewProof()
+{
+ d_current = d_proofs.allocateProof();
+}
+void CADProofGenerator::startRecursive() { d_current->openChild(); }
+void CADProofGenerator::endRecursive()
+{
+ d_current->setCurrent(PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
+ d_current->closeChild();
+}
+void CADProofGenerator::startScope()
+{
+ d_current->openChild();
+ d_current->getCurrent().d_rule = PfRule::SCOPE;
+}
+void CADProofGenerator::endScope(const std::vector<Node>& args)
+{
+ d_current->setCurrent(PfRule::SCOPE, {}, args, d_false);
+ d_current->closeChild();
+}
+
+ProofGenerator* CADProofGenerator::getProofGenerator() const
+{
+ return d_current;
+}
+
+void CADProofGenerator::addDirect(Node var,
+ VariableMapper& vm,
+ const poly::Polynomial& poly,
+ const poly::Assignment& a,
+ poly::SignCondition& sc,
+ const poly::Interval& interval,
+ Node constraint)
+{
+ if (is_minus_infinity(get_lower(interval))
+ && is_plus_infinity(get_upper(interval)))
+ {
+ // "Full conflict", constraint excludes (-inf,inf)
+ d_current->openChild();
+ d_current->setCurrent(
+ PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+ d_current->closeChild();
+ return;
+ }
+ std::vector<Node> res;
+ auto roots = poly::isolate_real_roots(poly, a);
+ if (get_lower(interval) == get_upper(interval))
+ {
+ // Excludes a single point only
+ auto ids = getRootIDs(roots, get_lower(interval));
+ Assert(ids.first == ids.second);
+ res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
+ }
+ else
+ {
+ // Excludes an open interval
+ if (!is_minus_infinity(get_lower(interval)))
+ {
+ // Interval has lower bound that is not -inf
+ auto ids = getRootIDs(roots, get_lower(interval));
+ Assert(ids.first == ids.second);
+ Kind rel = poly::get_lower_open(interval) ? Kind::GT : Kind::GEQ;
+ res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
+ }
+ if (!is_plus_infinity(get_upper(interval)))
+ {
+ // Interval has upper bound that is not inf
+ auto ids = getRootIDs(roots, get_upper(interval));
+ Assert(ids.first == ids.second);
+ Kind rel = poly::get_upper_open(interval) ? Kind::LT : Kind::LEQ;
+ res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
+ }
+ }
+ // Add to proof manager
+ startScope();
+ d_current->openChild();
+ d_current->setCurrent(
+ PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+ d_current->closeChild();
+ endScope(res);
+}
+
+std::vector<Node> CADProofGenerator::constructCell(Node var,
+ const CACInterval& i,
+ const poly::Assignment& a,
+ const poly::Value& s,
+ VariableMapper& vm)
+{
+ if (is_minus_infinity(get_lower(i.d_interval))
+ && is_plus_infinity(get_upper(i.d_interval)))
+ {
+ // "Full conflict", constraint excludes (-inf,inf)
+ return {};
+ }
+
+ std::vector<Node> res;
+
+ // Just use bounds for all polynomials
+ for (const auto& poly : i.d_mainPolys)
+ {
+ auto roots = poly::isolate_real_roots(poly, a);
+ auto ids = getRootIDs(roots, s);
+ if (ids.first == ids.second)
+ {
+ // Excludes a single point only
+ res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
+ }
+ else
+ {
+ // Excludes an open interval
+ if (ids.first > 0)
+ {
+ // Interval has lower bound that is not -inf
+ res.emplace_back(mkIRP(var, Kind::GT, d_zero, ids.first, poly, vm));
+ }
+ if (ids.second <= roots.size())
+ {
+ // Interval has upper bound that is not inf
+ res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.first, poly, vm));
+ }
+ }
+ }
+
+ return res;
+}
+
+std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
+{
+ return os << *proof.d_current;
+}
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
--- /dev/null
+/********************* */
+/*! \file proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Implements the proof generator for CAD
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#define CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+
+#include "util/real_algebraic_number.h"
+
+#ifdef CVC4_POLY_IMP
+
+#include <poly/polyxx.h>
+
+#include <vector>
+
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_set.h"
+#include "theory/arith/nl/cad/cdcac_utils.h"
+#include "theory/arith/nl/poly_conversion.h"
+#include "theory/lazy_tree_proof_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * This class manages the proof creation during a run of the CAD solver.
+ *
+ * Though it implements the ProofGenerator interface getProofFor(Node), it only
+ * gives a proof for a single node.
+ *
+ * It uses a LazyTreeProofGenerator internally to manage the tree-based proof
+ * construction.
+ */
+class CADProofGenerator
+{
+ public:
+ friend std::ostream& operator<<(std::ostream& os,
+ const CADProofGenerator& proof);
+ CADProofGenerator(context::Context* ctx, ProofNodeManager* pnm);
+
+ /** Start a new proof in this proof generator */
+ void startNewProof();
+ /** Start a new recursive call */
+ void startRecursive();
+ /** Finish the current recursive call */
+ void endRecursive();
+ /** Start a new scope, corresponding to a guess in CDCAC */
+ void startScope();
+ /** Finish a scope and add the (generalized) sample that was refuted */
+ void endScope(const std::vector<Node>& args);
+ /** Return the current proof generator */
+ ProofGenerator* getProofGenerator() const;
+
+ /**
+ * Calls LazyTreeProofGenerator::pruneChildren(f), but decorates the
+ * predicate such that f only accepts the index.
+ * @param f A Callable bool(std::size_t)
+ */
+ template <typename F>
+ void pruneChildren(F&& f)
+ {
+ d_current->pruneChildren(
+ [&f](std::size_t i, const detail::TreeProofNode& tpn) { return f(i); });
+ }
+
+ /**
+ * Add a direct interval conflict as generated in getUnsatIntervals().
+ * Its meaning is:
+ * over the partial assignment a, var is not in interval because p~sc~0
+ * and the origin of this is constraint.
+ *
+ * @param var The variable for which the interval is excluded
+ * @param vm A variable mapper between CVC4 and libpoly variables
+ * @param p The polynomial of the constraint
+ * @param a The current partial assignment
+ * @param sc The sign condition of the constraint
+ * @param interval The concrete interval that is excluded
+ * @param constraint The assumption that yields p and sc
+ */
+ void addDirect(Node var,
+ VariableMapper& vm,
+ const poly::Polynomial& p,
+ const poly::Assignment& a,
+ poly::SignCondition& sc,
+ const poly::Interval& interval,
+ Node constraint);
+
+ /**
+ * Constructs the (generalized) interval that is to be excluded from a
+ * CACInterval. It should be called after the recursive call to construct the
+ * generalized sample necessary for endScope().
+ *
+ * @param var The variable for which the interval is excluded
+ * @param i The concrete interval that is excluded
+ * @param a The current partial assignment
+ * @param s The sample point that is refuted for var
+ * @param vm A variable mapper between CVC4 and libpoly variables
+ */
+ std::vector<Node> constructCell(Node var,
+ const CACInterval& i,
+ const poly::Assignment& a,
+ const poly::Value& s,
+ VariableMapper& vm);
+
+ private:
+ /** The proof node manager used for the proofs */
+ ProofNodeManager* d_pnm;
+ /** The list of generated proofs */
+ CDProofSet<LazyTreeProofGenerator> d_proofs;
+ /** The current proof */
+ LazyTreeProofGenerator* d_current;
+
+ /** Constant false */
+ Node d_false;
+ /** Constant zero */
+ Node d_zero;
+};
+
+/**
+ * Prints the underlying LazyTreeProofGenerator. Please check the documentation
+ * of std::ostream& operator<<(std::ostream&, const LazyTreeProofGenerator&)
+ */
+std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof);
+
+} // namespace cad
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
+#endif
projects / cvc5.git / commitdiff