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
}
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) {
#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"
// 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;
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
: 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()) {
#include "theory/theory.h"
#include "expr/node.h"
+#include "proof/arith_proof_recorder.h"
#include "theory/arith/theory_arith_private_forward.h"
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);
const EntailmentCheckParameters* params,
EntailmentCheckSideEffects* out) override;
+ void setProofRecorder(proof::ArithProofRecorder * proofRecorder)
+ {
+ d_proofRecorder = proofRecorder;
+ }
+
};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
projects / cvc5.git / commitdiff