diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/proof/arith_proof.cpp | 6 | ||||
| -rw-r--r-- | src/proof/arith_proof.h | 6 | ||||
| -rw-r--r-- | src/proof/arith_proof_recorder.cpp | 81 | ||||
| -rw-r--r-- | src/proof/arith_proof_recorder.h | 107 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 1 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 11 |
7 files changed, 212 insertions, 2 deletions
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 <unordered_set> #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 <algorithm> +#include <vector> + +#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<Node> 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<Node>& conflict) const +{ + return d_lemmasToFarkasCoefficients.find(conflict) + != d_lemmasToFarkasCoefficients.end(); +} + +std::pair<Node, theory::arith::RationalVectorCP> +ArithProofRecorder::getFarkasCoefficients(const std::set<Node>& 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 <map> +#include <set> + +#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<Node>& 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<Node, theory::arith::RationalVectorCP> getFarkasCoefficients( + const std::set<Node>& conflict) const; + + protected: + // For each lemma, save the Farkas coefficients of that lemma + std::map<std::set<Node>, std::pair<Node, theory::arith::RationalVector>> + 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 */ |