From 7a695fd7c29af97dbcc363eb277ffeae1617cffe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 23 Feb 2021 17:17:45 +0100 Subject: [PATCH] (proof-new) Add proof generator for CAD solver (#5964) 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. --- src/CMakeLists.txt | 4 + src/expr/proof_rule.cpp | 2 + src/expr/proof_rule.h | 35 +++ src/theory/arith/nl/cad/proof_checker.cpp | 61 +++++ src/theory/arith/nl/cad/proof_checker.h | 59 +++++ src/theory/arith/nl/cad/proof_generator.cpp | 232 ++++++++++++++++++++ src/theory/arith/nl/cad/proof_generator.h | 149 +++++++++++++ 7 files changed, 542 insertions(+) create mode 100644 src/theory/arith/nl/cad/proof_checker.cpp create mode 100644 src/theory/arith/nl/cad/proof_checker.h create mode 100644 src/theory/arith/nl/cad/proof_generator.cpp create mode 100644 src/theory/arith/nl/cad/proof_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5a44df141..deb20ab70 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -347,6 +347,10 @@ libcvc4_add_sources( 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 diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 85463d2d9..bead7397a 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -188,6 +188,8 @@ const char* toString(PfRule id) 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 "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 917db4088..d42175fab 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1277,6 +1277,41 @@ enum class PfRule : uint32_t // 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, }; diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp new file mode 100644 index 000000000..24c4b813c --- /dev/null +++ b/src/theory/arith/nl/cad/proof_checker.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \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& children, + const std::vector& 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 diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h new file mode 100644 index 000000000..d10ce2e1b --- /dev/null +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \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& children, + const std::vector& args) override; +}; + +} // namespace cad +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp new file mode 100644 index 000000000..ebf1ab25e --- /dev/null +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -0,0 +1,232 @@ +/********************* */ +/*! \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 getRootIDs( + const std::vector& 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(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(false); + d_zero = NodeManager::currentNM()->mkConst(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& 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 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 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 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 diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h new file mode 100644 index 000000000..fd2458271 --- /dev/null +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -0,0 +1,149 @@ +/********************* */ +/*! \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 + +#include + +#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& 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 + 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 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 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 -- 2.30.2