From 4983fb0e4339d1c03c8eb5567aca566a378114ea Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 14 Dec 2018 17:44:39 -0800 Subject: [PATCH] [LRA Proof] Storage for LRA proofs (#2747) * [LRA Proof] Storage for LRA proofs During LRA solving the `ConstraintDatabase` contains the reasoning behind different constraints. Combinations of constraints are periodically used to justify lemmas (conflict clauses, propegations, ... ?). `ConstraintDatabase` is SAT context-dependent. ArithProofRecorder will be used to store concise representations of the proof for each lemma raised by the (LR)A theory. The (LR)A theory will write to it, and the ArithProof class will read from it to produce LFSC proofs. Right now, it's pretty simplistic -- it allows for only Farkas proofs. In future PRs I'll: 1. add logic that stores proofs therein 2. add logic that retrieves and prints proofs 3. enable LRA proof production, checking, and testing * Document ArithProofRecorder use-sites * Update src/proof/arith_proof_recorder.cpp Co-Authored-By: alex-ozdemir * Yoni's review * clang-format * Response to Mathias' review. --- src/CMakeLists.txt | 2 + src/proof/arith_proof.cpp | 6 +- src/proof/arith_proof.h | 6 ++ src/proof/arith_proof_recorder.cpp | 81 ++++++++++++++++++++++ src/proof/arith_proof_recorder.h | 107 +++++++++++++++++++++++++++++ src/theory/arith/theory_arith.cpp | 1 + src/theory/arith/theory_arith.h | 11 +++ 7 files changed, 212 insertions(+), 2 deletions(-) create mode 100644 src/proof/arith_proof_recorder.cpp create mode 100644 src/proof/arith_proof_recorder.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 91c06ddd9..7ecee2dee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -124,6 +124,8 @@ libcvc4_add_sources( printer/tptp/tptp_printer.h proof/arith_proof.cpp proof/arith_proof.h + proof/arith_proof_recorder.cpp + proof/arith_proof_recorder.h proof/array_proof.cpp proof/array_proof.h proof/bitvector_proof.cpp diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 3b57be1f2..1d51f99e1 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -640,8 +640,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, } ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe) - : TheoryProof(arith, pe), d_realMode(false) -{} + : TheoryProof(arith, pe), d_recorder(), d_realMode(false) +{ + arith->setProofRecorder(&d_recorder); +} theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; } void ArithProof::registerTerm(Expr term) { diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 27012184a..a58294998 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -23,6 +23,7 @@ #include #include "expr/expr.h" +#include "proof/arith_proof_recorder.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "theory/uf/equality_engine.h" @@ -62,6 +63,11 @@ protected: // TypeSet d_sorts; // all the uninterpreted sorts in this theory ExprSet d_declarations; // all the variable/function declarations + /** + * @brief Where farkas proofs of lemmas are stored. + */ + proof::ArithProofRecorder d_recorder; + bool d_realMode; theory::TheoryId getTheoryId() override; diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp new file mode 100644 index 000000000..d654ea073 --- /dev/null +++ b/src/proof/arith_proof_recorder.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file arith_proof_recorder.cpp + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 A class for recording the skeletons of arithmetic proofs at solve + ** time so they can later be used during proof-production time. + **/ + +#include "proof/arith_proof_recorder.h" + +#include +#include + +#include "base/map_util.h" + +namespace CVC4 { +namespace proof { + +ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients() +{ + // Nothing else +} +void ArithProofRecorder::saveFarkasCoefficients( + Node conflict, theory::arith::RationalVectorCP farkasCoefficients) +{ + Assert(conflict.getKind() == kind::AND); + Assert(conflict.getNumChildren() == farkasCoefficients->size()); + for (size_t i = 0; i < conflict.getNumChildren(); ++i) + { + const Node& child = conflict[i]; + Assert(child.getType().isBoolean() && child[0].getType().isReal()); + } + Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl; + if (Debug.isOn("pf::arith")) + { + for (size_t i = 0; i < conflict.getNumChildren(); ++i) + { + const Node& child = conflict[i]; + const Rational& r = (*farkasCoefficients)[i]; + Debug("pf::arith") << " " << std::setw(8) << r; + Debug("pf::arith") << " " << child << std::endl; + } + } + + std::set lits; + std::copy( + conflict.begin(), conflict.end(), std::inserter(lits, lits.begin())); + + d_lemmasToFarkasCoefficients[lits] = + std::make_pair(std::move(conflict), *farkasCoefficients); +} + +bool ArithProofRecorder::hasFarkasCoefficients( + const std::set& conflict) const +{ + return d_lemmasToFarkasCoefficients.find(conflict) + != d_lemmasToFarkasCoefficients.end(); +} + +std::pair +ArithProofRecorder::getFarkasCoefficients(const std::set& conflict) const +{ + if (auto *p = FindOrNull(d_lemmasToFarkasCoefficients, conflict)) + { + return std::make_pair(p->first, &p->second); + } + else + { + return std::make_pair(Node(), theory::arith::RationalVectorCPSentinel); + } +} + +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h new file mode 100644 index 000000000..2d0501332 --- /dev/null +++ b/src/proof/arith_proof_recorder.h @@ -0,0 +1,107 @@ +/********************* */ +/*! \file arith_proof_recorder.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 A class for recording the skeletons of arithmetic proofs at solve + ** time so they can later be used during proof-production time. + ** + ** In particular, we're interested in proving bottom from a conjunction of + ** theory literals. + ** + ** For now, we assume that this can be done using a Farkas combination, and if + ** that doesn't work for some reason, then we give up and "trust" the lemma. + ** In the future we'll build support for more sophisticated reasoning. + ** + ** Given this scope, our task is to... + ** for each lemma (a set of literals) + ** save the Farkas coefficients for those literals + ** which requires we save an ordering of the literals + ** and a parallel ordering of Farkas coefficients. + ** + ** Farkas proofs have the following core structure: + ** For a list of affine bounds: c[i] dot x >= b[i] + ** (x is a vector of variables) + ** (c[i] is a vector of coefficients) + ** and a list of non-negative coefficients: f[i], + ** compute + ** + ** sum_i{ (c[i] dot x) * f[i] } and sum_i{b[i]*f[i]} + ** + ** and then verify that the left is actually < the right, a contradiction + ** + ** To be clear: this code does not check Farkas proofs, it just stores the + ** information needed to write them. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H +#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H + +#include +#include + +#include "expr/node.h" +#include "theory/arith/constraint_forward.h" + +namespace CVC4 { +namespace proof { + +class ArithProofRecorder +{ + public: + ArithProofRecorder(); + + /** + * @brief For a set of incompatible literals, save the Farkas coefficients + * demonstrating their incompatibility + * + * @param conflict a conjunction of conflicting literals + * @param farkasCoefficients a list of rational coefficients which the literals + * should be multiplied by (pairwise) to produce a contradiction. + * + * The orders of the two vectors must agree! + */ + void saveFarkasCoefficients( + Node conflict, theory::arith::RationalVectorCP farkasCoefficients); + + /** + * @brief Determine whether some literals have a Farkas proof of their + * incompatibility + * + * @param conflict a conjunction of (putatively) conflicting literals + * + * @return whether or not there is actually a proof for them. + */ + bool hasFarkasCoefficients(const std::set& conflict) const; + + /** + * @brief Get the Farkas Coefficients object + * + * @param conflict a conjunction of conflicting literals + * @return theory::arith::RationalVectorCP -- the Farkas coefficients + * Node -- a conjunction of the problem literals in coefficient order + * + * theory::arith::RationalVectorCPSentinel if there is no entry for + * these lits + */ + std::pair getFarkasCoefficients( + const std::set& conflict) const; + + protected: + // For each lemma, save the Farkas coefficients of that lemma + std::map, std::pair> + d_lemmasToFarkasCoefficients; +}; + +} // namespace proof +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d7113b17d..9902121d0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -36,6 +36,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) , d_ppRewriteTimer("theory::arith::ppRewriteTimer") + , d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); if (options::nlExt()) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 195cb1883..e4b1c5b26 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -19,6 +19,7 @@ #include "theory/theory.h" #include "expr/node.h" +#include "proof/arith_proof_recorder.h" #include "theory/arith/theory_arith_private_forward.h" @@ -40,6 +41,11 @@ private: TimerStat d_ppRewriteTimer; + /** + * @brief Where to store Farkas proofs of lemmas + */ + proof::ArithProofRecorder * d_proofRecorder; + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -90,6 +96,11 @@ public: const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) override; + void setProofRecorder(proof::ArithProofRecorder * proofRecorder) + { + d_proofRecorder = proofRecorder; + } + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ -- 2.30.2