proof/array_proof.h
proof/bitvector_proof.cpp
proof/bitvector_proof.h
+ proof/clausal_bitvector_proof.cpp
+ proof/clausal_bitvector_proof.h
proof/clause_id.h
proof/cnf_proof.cpp
proof/cnf_proof.h
#include "options/proof_options.h"
#include "proof/proof_output_channel.h"
#include "proof/theory_proof.h"
+#include "prop/sat_solver_types.h"
#include "theory/bv/bitblast/bitblaster.h"
#include "theory/bv/theory_bv.h"
namespace CVC4 {
+
+namespace proof {
BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine)
: TheoryProof(bv, proofEngine),
return os.str();
}
-void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
- context::Context* cnf)
-{
- Assert(d_cnfProof == nullptr);
- d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
-}
-
void BitVectorProof::printOwnedTerm(Expr term,
std::ostream& os,
const ProofLetMap& map)
}
}
+theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; }
+
const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof()
{
return &d_atomsInBitblastingProof;
os << ")";
}
+} // namespace proof
+
} // namespace CVC4
#include <unordered_map>
#include <unordered_set>
#include <vector>
+
#include "expr/expr.h"
#include "proof/cnf_proof.h"
#include "proof/theory_proof.h"
-#include "theory/bv/bitblast/bitblaster.h"
+#include "prop/sat_solver.h"
#include "theory/bv/theory_bv.h"
+// Since TBitblaster and BitVectorProof are cyclically dependent, we need this
+// forward declaration
+namespace CVC4 {
+namespace theory {
+namespace bv {
+template <class T>
+class TBitblaster;
+}
+} // namespace theory
+} // namespace CVC4
+
namespace CVC4 {
+namespace proof {
+
typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
*/
std::unique_ptr<CnfProof> d_cnfProof;
+ theory::TheoryId getTheoryId() override;
+
public:
void printOwnedTerm(Expr term,
std::ostream& os,
*/
virtual void calculateAtomsInBitblastingProof() = 0;
+ /**
+ * Prints out a declaration of the bit-blasting, and the subsequent
+ * conversion of the result to CNF
+ *
+ * @param os the stream to print to
+ * @param paren a stream that will be placed at the back of the proof (for
+ * closing parens)
+ * @param letMap The let-map, which contains information about LFSC
+ * identifiers and the values they reference.
+ */
+ virtual void printBBDeclarationAndCnf(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) = 0;
+
+ /**
+ * Prints a proof of the empty clause.
+ *
+ * @param os the stream to print to
+ * @param paren any parentheses to add to the end of the global proof
+ */
+ virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+
/**
* Read the d_atomsInBitblastingProof member.
* See its documentation.
/**
* This must be done before registering any terms or atoms, since the CNF
* proof must reflect the result of bitblasting those
+ *
+ * Feeds the SAT solver's true and false variables into the CNF stream.
*/
- virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
+ virtual void initCnfProof(prop::CnfStream* cnfStream,
+ context::Context* cnf,
+ prop::SatVariable trueVar,
+ prop::SatVariable falseVar) = 0;
CnfProof* getCnfProof() { return d_cnfProof.get(); }
+ /**
+ * Attaches this BVP to the given SAT solver, initializing a SAT proof.
+ *
+ * This must be invoked before `initCnfProof` because a SAT proof must already
+ * exist to initialize a CNF proof.
+ */
+ virtual void attachToSatSolver(prop::SatSolver& sat_solver) = 0;
+
void setBitblaster(theory::bv::TBitblaster<Node>* bb);
+ /**
+ * Kind of a mess. Used for resulution-based BVP's, where in eager mode this
+ * must be invoked before printing a proof of the empty clause. In lazy mode
+ * the behavior and purpose are both highly unclear.
+ *
+ * This exists as a virtual method of BitVectorProof, and not
+ * ResolutionBitVectorProof, because the machinery that invokes it is
+ * high-level enough that it doesn't know the difference between clausal and
+ * resolution proofs.
+ *
+ * TODO(aozdemir) figure out what is going on and clean this up
+ * Issue: https://github.com/CVC4/CVC4/issues/2789
+ */
+ virtual void finalizeConflicts(std::vector<Expr>& conflicts){};
+
private:
ExprToString d_exprToVariableName;
const Node& n2) override;
};
+} // namespace proof
+
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR__PROOF_H */
--- /dev/null
+/********************* */
+/*! \file clausal_bitvector_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Bitvector proof using the DRAT proof format
+ **
+ ** Contains DRAT-specific printing logic.
+ **/
+
+#include "cvc4_private.h"
+
+#include <algorithm>
+#include <iterator>
+#include <set>
+#include "options/bv_options.h"
+#include "proof/clausal_bitvector_proof.h"
+#include "proof/drat/drat_proof.h"
+#include "proof/lfsc_proof_printer.h"
+#include "theory/bv/theory_bv.h"
+
+namespace CVC4 {
+
+namespace proof {
+
+ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine)
+ : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+{
+}
+
+void ClausalBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver)
+{
+ sat_solver.setClausalProofLog(this);
+}
+
+void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+ context::Context* cnf,
+ prop::SatVariable trueVar,
+ prop::SatVariable falseVar)
+{
+ Assert(d_cnfProof == nullptr);
+ d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
+
+ // Create a clause which forces the true variable to be true, and register it
+ int trueClauseId = ClauseId(ProofManager::currentPM()->nextId());
+ // with the CNF proof
+ d_cnfProof->registerTrueUnitClause(trueClauseId);
+ // and with (this) bit-vector proof
+ prop::SatClause c{prop::SatLiteral(trueVar, false)};
+ registerUsedClause(trueClauseId, c);
+
+ // The same for false.
+ int falseClauseId = ClauseId(ProofManager::currentPM()->nextId());
+ d_cnfProof->registerFalseUnitClause(falseClauseId);
+ c[0] = prop::SatLiteral(falseVar, true);
+ registerUsedClause(falseClauseId, c);
+}
+
+void ClausalBitVectorProof::registerUsedClause(ClauseId id,
+ prop::SatClause& clause)
+{
+ d_usedClauses.emplace_back(
+ id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+};
+
+void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
+{
+ if (Debug.isOn("bv::clausal"))
+ {
+ std::string serializedDratProof = d_binaryDratProof.str();
+ Debug("bv::clausal") << "binary DRAT proof byte count: "
+ << serializedDratProof.size() << std::endl;
+ Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
+ drat::DratProof dratProof =
+ drat::DratProof::fromBinary(serializedDratProof);
+
+ Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
+ dratProof.outputAsText(Debug("bv::clausal"));
+ }
+ Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map)
+{
+ Unreachable(
+ "Clausal bit-vector proofs should only be used in combination with eager "
+ "bitblasting, which **does not use theory lemmas**");
+}
+
+void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap)
+{
+ Unimplemented();
+}
+
+void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
+{
+ Unimplemented();
+}
+
+} // namespace proof
+
+}; // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file clausal_bitvector_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Bitvector proof for clausal (DRAT/LRAT) formats
+ **
+ ** An internal string stream is hooked up to CryptoMiniSat, which spits out a
+ ** binary DRAT proof. Depending on which kind of proof we're going to turn
+ ** that into, we process it in different ways.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+
+#include <iostream>
+#include <sstream>
+#include <unordered_map>
+
+#include "expr/expr.h"
+#include "proof/bitvector_proof.h"
+#include "proof/drat/drat_proof.h"
+#include "proof/lrat/lrat_proof.h"
+#include "proof/theory_proof.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/theory_bv.h"
+
+namespace CVC4 {
+
+namespace proof {
+
+class ClausalBitVectorProof : public BitVectorProof
+{
+ public:
+ ClausalBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine);
+
+ ~ClausalBitVectorProof() = default;
+
+ void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
+ void initCnfProof(prop::CnfStream* cnfStream,
+ context::Context* cnf,
+ prop::SatVariable trueVar,
+ prop::SatVariable falseVar) override;
+
+ std::ostream& getDratOstream() { return d_binaryDratProof; }
+
+ void registerUsedClause(ClauseId id, prop::SatClause& clause);
+
+ void calculateAtomsInBitblastingProof() override;
+
+ protected:
+ // A list of all clauses and their ids which are passed into the SAT solver
+ std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
+ d_usedClauses;
+ // Stores the proof recieved from the SAT solver.
+ std::ostringstream d_binaryDratProof;
+};
+
+/**
+ * A representation of a clausal proof of a bitvector problem's UNSAT nature
+ */
+class LfscClausalBitVectorProof : public ClausalBitVectorProof
+{
+ public:
+ LfscClausalBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine)
+ : ClausalBitVectorProof(bv, proofEngine)
+ {
+ // That's all!
+ }
+
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printBBDeclarationAndCnf(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) override;
+ void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+} // namespace proof
+
+} // namespace CVC4
+
+#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
setClauseDefinition(clause, current_expr);
}
+void CnfProof::registerTrueUnitClause(ClauseId clauseId)
+{
+ Node trueNode = NodeManager::currentNM()->mkConst<bool>(true);
+ pushCurrentAssertion(trueNode);
+ pushCurrentDefinition(trueNode);
+ registerConvertedClause(clauseId);
+ popCurrentAssertion();
+ popCurrentDefinition();
+ d_cnfStream->ensureLiteral(trueNode);
+ d_trueUnitClause = clauseId;
+}
+
+void CnfProof::registerFalseUnitClause(ClauseId clauseId)
+{
+ Node falseNode = NodeManager::currentNM()->mkConst<bool>(false).notNode();
+ pushCurrentAssertion(falseNode);
+ pushCurrentDefinition(falseNode);
+ registerConvertedClause(clauseId);
+ popCurrentAssertion();
+ popCurrentDefinition();
+ d_cnfStream->ensureLiteral(falseNode);
+ d_falseUnitClause = clauseId;
+}
+
void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
Debug("proof:cnf") << "CnfProof::setClauseAssertion "
<< clause << " assertion " << expr << std::endl;
ClauseIdSet d_explanations;
+ // The clause ID of the unit clause defining the true SAT literal.
+ ClauseId d_trueUnitClause;
+ // The clause ID of the unit clause defining the false SAT literal.
+ ClauseId d_falseUnitClause;
+
bool isDefinition(Node node);
Node getDefinitionForClause(ClauseId clause);
// already in CNF
void registerConvertedClause(ClauseId clause, bool explanation=false);
+ // The CNF proof has a special relationship to true and false.
+ // In particular, it need to know the identity of clauses defining
+ // canonical true and false literals in the underlying SAT solver.
+ void registerTrueUnitClause(ClauseId clauseId);
+ void registerFalseUnitClause(ClauseId clauseId);
+ inline ClauseId getTrueUnitClause() { return d_trueUnitClause; };
+ inline ClauseId getFalseUnitClause() { return d_falseUnitClause; };
+
/** Clause is one of the clauses defining the node expression*/
void setClauseDefinition(ClauseId clause, Node node);
#include "proof/proof_utils.h"
#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/bvminisat.h"
+#include "prop/sat_solver_types.h"
#include "theory/bv/bitblast/bitblaster.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_rewrite_rules.h"
d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true));
}
-theory::TheoryId ResolutionBitVectorProof::getTheoryId()
+void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
+ context::Context* cnf,
+ prop::SatVariable trueVar,
+ prop::SatVariable falseVar)
{
- return theory::THEORY_BV;
+ Assert(d_resolutionProof != NULL);
+ Assert(d_cnfProof == nullptr);
+ d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb"));
+
+ d_cnfProof->registerTrueUnitClause(d_resolutionProof->getTrueUnit());
+ d_cnfProof->registerFalseUnitClause(d_resolutionProof->getFalseUnit());
}
-void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
- context::Context* cnf)
+void ResolutionBitVectorProof::attachToSatSolver(prop::SatSolver& sat_solver)
{
- Assert(d_resolutionProof != NULL);
- BitVectorProof::initCnfProof(cnfStream, cnf);
-
- // true and false have to be setup in a special way
- Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
- Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
-
- d_cnfProof->pushCurrentAssertion(true_node);
- d_cnfProof->pushCurrentDefinition(true_node);
- d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit());
- d_cnfProof->popCurrentAssertion();
- d_cnfProof->popCurrentDefinition();
-
- d_cnfProof->pushCurrentAssertion(false_node);
- d_cnfProof->pushCurrentDefinition(false_node);
- d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit());
- d_cnfProof->popCurrentAssertion();
- d_cnfProof->popCurrentDefinition();
+ sat_solver.setResolutionProofLog(this);
}
BVSatProof* ResolutionBitVectorProof::getSatProof()
}
}
-void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
- std::ostream& os,
- std::ostream& paren,
- const ProofLetMap& map)
+void LfscResolutionBitVectorProof::printTheoryLemmaProof(
+ std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map)
{
- Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called"
- << std::endl;
+ Debug("pf::bv")
+ << "(pf::bv) LfscResolutionBitVectorProof::printTheoryLemmaProof called"
+ << std::endl;
Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
}
}
-void LFSCBitVectorProof::calculateAtomsInBitblastingProof()
+void LfscResolutionBitVectorProof::calculateAtomsInBitblastingProof()
{
// Collect the input clauses used
IdToSatClause used_lemmas;
Assert(used_lemmas.empty());
}
-void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
- std::ostream& paren,
- ProofLetMap& letMap)
+void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap)
{
// print mapping between theory atoms and internal SAT variables
os << std::endl << ";; BB atom mapping\n" << std::endl;
proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren);
}
-} /* namespace proof */
+void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os,
+ std::ostream& paren)
+{
+ Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+ "the BV theory should only be proving bottom directly in the eager "
+ "bitblasting mode");
+ proof::LFSCProofPrinter::printResolutionEmptyClause(
+ d_resolutionProof.get(), os, paren);
+}
+
+} // namespace proof
} /* namespace CVC4 */
#include "context/context.h"
#include "expr/expr.h"
#include "proof/bitvector_proof.h"
+#include "proof/sat_proof.h"
#include "proof/theory_proof.h"
#include "prop/bvminisat/core/Solver.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver_types.h"
+#include "theory/bv/bitblast/bitblaster.h"
+#include "theory/bv/theory_bv.h"
namespace CVC4 {
-namespace theory {
-namespace bv {
-class TheoryBV;
-template <class T>
-class TBitblaster;
-} // namespace bv
-} // namespace theory
-
-// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
-// header cycle and remove this.
-namespace prop {
-class CnfStream;
-}
-
-} /* namespace CVC4 */
-
-
-namespace CVC4 {
-
-template <class Solver>
-class TSatProof;
typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
namespace proof {
BVSatProof* getSatProof();
- /**
- * Kind of a mess.
- * In eager mode this must be invoked before printing a proof of the empty
- * clause. In lazy mode the behavior is ???
- * TODO(aozdemir) clean this up.
- */
- void finalizeConflicts(std::vector<Expr>& conflicts);
+ void finalizeConflicts(std::vector<Expr>& conflicts) override;
void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
void markAssumptionConflict() { d_isAssumptionConflict = true; }
bool isAssumptionConflict() const { return d_isAssumptionConflict; }
- virtual void printResolutionProof(std::ostream& os,
- std::ostream& paren,
- ProofLetMap& letMap) = 0;
-
- void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
+ void initCnfProof(prop::CnfStream* cnfStream,
+ context::Context* cnf,
+ prop::SatVariable trueVar,
+ prop::SatVariable falseVar) override;
protected:
+ void attachToSatSolver(prop::SatSolver& sat_solver) override;
+
context::Context d_fakeContext;
// The CNF formula that results from bit-blasting will need a proof.
bool d_isAssumptionConflict;
- theory::TheoryId getTheoryId() override;
};
-class LFSCBitVectorProof : public ResolutionBitVectorProof
+class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
{
public:
- LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+ LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv,
+ TheoryProofEngine* proofEngine)
: ResolutionBitVectorProof(bv, proofEngine)
{
}
std::ostream& os,
std::ostream& paren,
const ProofLetMap& map) override;
- void printResolutionProof(std::ostream& os,
- std::ostream& paren,
- ProofLetMap& letMap) override;
+ void printBBDeclarationAndCnf(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) override;
+ void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
void calculateAtomsInBitblastingProof() override;
};
#include "options/proof_options.h"
#include "proof/arith_proof.h"
#include "proof/array_proof.h"
+#include "proof/clausal_bitvector_proof.h"
#include "proof/clause_id.h"
#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
namespace CVC4 {
-using proof::LFSCBitVectorProof;
+using proof::LfscResolutionBitVectorProof;
using proof::ResolutionBitVectorProof;
unsigned CVC4::ProofLetCount::counter = 0;
}
if (id == theory::THEORY_BV) {
- auto bv_theory = static_cast<theory::bv::TheoryBV*>(th);
- ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this);
- d_theoryProofTable[id] = bvp;
+ auto thBv = static_cast<theory::bv::TheoryBV*>(th);
+ if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+ && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
+ {
+ proof::BitVectorProof* bvp =
+ new proof::LfscClausalBitVectorProof(thBv, this);
+ d_theoryProofTable[id] = bvp;
+ }
+ else
+ {
+ proof::BitVectorProof* bvp =
+ new proof::LfscResolutionBitVectorProof(thBv, this);
+ d_theoryProofTable[id] = bvp;
+ }
return;
}
if (th) {
theory::TheoryId id = th->getId();
if (id == theory::THEORY_BV) {
+ theory::bv::TheoryBV* bv_th = static_cast<theory::bv::TheoryBV*>(th);
Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
- ResolutionBitVectorProof* bvp =
- (ResolutionBitVectorProof*)d_theoryProofTable[id];
- ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp);
+ proof::BitVectorProof* bvp =
+ static_cast<proof::BitVectorProof*>(d_theoryProofTable[id]);
+ bv_th->setProofLog(bvp);
return;
}
}
}
}
- ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof();
+ proof::BitVectorProof* bv = ProofManager::getBitVectorProof();
bv->finalizeConflicts(bv_lemmas);
- // bv->printResolutionProof(os, paren, letMap);
}
void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
}
// finalizeBvConflicts(lemmas, os, paren, map);
- ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map);
+ ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map);
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
Assert (lemmas.size() == 1);
d_minisat->popAssumption();
}
-void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BVMinisatSatSolver::setResolutionProofLog(
+ proof::ResolutionBitVectorProof* bvp)
{
d_minisat->setProofLog( bvp );
}
void popAssumption() override;
- void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+ void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
private:
/* Disable the default constructor. */
}
}
- PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node););
+ if (PROOF_ON() && d_cnfProof)
+ {
+ d_cnfProof->pushCurrentDefinition(node);
+ }
ClauseId clause_id = d_satSolver->addClause(c, d_removable);
if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
- PROOF
- (
- if (d_cnfProof) {
- Assert (clause_id != ClauseIdError);
- d_cnfProof->registerConvertedClause(clause_id);
- d_cnfProof->popCurrentDefinition();
- }
- );
+ if (PROOF_ON() && d_cnfProof)
+ {
+ if (clause_id != ClauseIdError)
+ {
+ d_cnfProof->registerConvertedClause(clause_id);
+ }
+ d_cnfProof->popCurrentDefinition();
+ };
}
void CnfStream::assertClause(TNode node, SatLiteral a) {
CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
const std::string& name)
-: d_solver(new CMSat::SATSolver())
-, d_numVariables(0)
-, d_okay(true)
-, d_statistics(registry, name)
+ : d_solver(new CMSat::SATSolver()),
+ d_bvp(nullptr),
+ d_numVariables(0),
+ d_okay(true),
+ d_statistics(registry, name)
{
d_true = newVar();
d_false = newVar();
std::vector<CMSat::Lit> internal_clause;
toInternalClause(clause, internal_clause);
- bool res = d_solver->add_clause(internal_clause);
- d_okay &= res;
- return ClauseIdError;
+ bool nowOkay = d_solver->add_clause(internal_clause);
+ ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
+
+ THEORY_PROOF(
+ // If this clause results in a conflict, then `nowOkay` may be false, but
+ // we still need to register this clause as used. Thus, we look at
+ // `d_okay` instead
+ if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+
+ d_okay &= nowOkay;
+ return freshId;
}
bool CryptoMinisatSolver::ok() const {
return -1;
}
+void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
+{
+ d_bvp = bvp;
+ d_solver->set_drat(&bvp->getDratOstream(), false);
+}
+
// Satistics for CryptoMinisatSolver
CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
#ifdef CVC4_USE_CRYPTOMINISAT
+#include "proof/clausal_bitvector_proof.h"
#include "prop/sat_solver.h"
// Cryptominisat has name clashes with the other Minisat implementations since
private:
std::unique_ptr<CMSat::SATSolver> d_solver;
+ proof::ClausalBitVectorProof* d_bvp;
unsigned d_numVariables;
bool d_okay;
SatVariable d_true;
SatValue modelValue(SatLiteral l) override;
unsigned getAssertionLevel() const override;
+ void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
class Statistics {
public:
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/node.h"
-#include "proof/resolution_bitvector_proof.h"
#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
#include "prop/bv_sat_solver_notify.h"
namespace CVC4 {
+namespace proof {
+class ClausalBitVectorProof;
+class ResolutionBitVectorProof;
+} // namespace proof
+
namespace prop {
class TheoryProxy;
/** Check if the solver is in an inconsistent state */
virtual bool ok() const = 0;
- virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+ virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
+
+ virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
};/* class SatSolver */
#include <vector>
#include "expr/node.h"
+#include "proof/bitvector_proof.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/bitblast/bitblast_strategies_template.h"
#include "theory/valuation.h"
#include "util/resource_manager.h"
+
namespace CVC4 {
namespace theory {
namespace bv {
// caches and mappings
TermDefMap d_termCache;
ModelCache d_modelCache;
+ // sat solver used for bitblasting and associated CnfStream
+ std::unique_ptr<context::Context> d_nullContext;
+ std::unique_ptr<prop::CnfStream> d_cnfStream;
+ proof::BitVectorProof* d_bvp;
void initAtomBBStrategies();
void initTermBBStrategies();
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0;
+ virtual prop::SatSolver* getSatSolver() = 0;
+
public:
TBitblaster();
bool hasBBTerm(TNode node) const;
void getBBTerm(TNode node, Bits& bits) const;
virtual void storeBBTerm(TNode term, const Bits& bits);
+ void setProofLog(proof::BitVectorProof* bvp);
+
/**
* Return a constant representing the value of a in the model.
* If fullModel is true set unconstrained bits to 0. If not return
}
template <class T>
-TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache()
+TBitblaster<T>::TBitblaster()
+ : d_termCache(),
+ d_modelCache(),
+ d_nullContext(new context::Context()),
+ d_cnfStream(),
+ d_bvp(nullptr)
{
initAtomBBStrategies();
initTermBBStrategies();
d_modelCache.clear();
}
+template <class T>
+void TBitblaster<T>::setProofLog(proof::BitVectorProof* bvp)
+{
+ if (THEORY_PROOF_ON())
+ {
+ d_bvp = bvp;
+ prop::SatSolver* satSolver = getSatSolver();
+ bvp->attachToSatSolver(*satSolver);
+ prop::SatVariable t = satSolver->trueVar();
+ prop::SatVariable f = satSolver->falseVar();
+ bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f);
+ }
+}
+
template <class T>
Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
{
EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
: TBitblaster<Node>(),
d_context(c),
- d_nullContext(new context::Context()),
d_satSolver(),
d_bitblastingRegistrar(new BitblastingRegistrar(this)),
- d_cnfStream(),
- d_bvp(nullptr),
d_bv(theory_bv),
d_bbAtoms(),
d_variables(),
return true;
}
-void EagerBitblaster::setResolutionProofLog(
- proof::ResolutionBitVectorProof* bvp)
-{
- THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp);
- bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());)
-}
-
bool EagerBitblaster::isSharedTerm(TNode node) {
return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
}
bool solve();
bool solve(const std::vector<Node>& assumptions);
bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
private:
context::Context* d_context;
- std::unique_ptr<context::Context> d_nullContext;
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- // sat solver used for bitblasting and associated CnfStream
std::unique_ptr<prop::SatSolver> d_satSolver;
std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
- std::unique_ptr<prop::CnfStream> d_cnfStream;
-
- BitVectorProof* d_bvp;
TheoryBV* d_bv;
TNodeSet d_bbAtoms;
std::unique_ptr<MinisatEmptyNotify> d_notify;
Node getModelFromSatSolver(TNode a, bool fullModel) override;
+ prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
bool isSharedTerm(TNode node);
};
bool emptyNotify)
: TBitblaster<Node>(),
d_bv(bv),
- d_bvp(nullptr),
d_ctx(c),
d_nullRegistrar(new prop::NullRegistrar()),
- d_nullContext(new context::Context()),
d_assertedAtoms(new (true) context::CDList<prop::SatLiteral>(c)),
d_explanations(new (true) ExplanationMap(c)),
d_variables(),
return true;
}
-void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void TLazyBitblaster::setProofLog(proof::BitVectorProof* bvp)
{
- d_bvp = bvp;
- d_satSolver->setProofLog( bvp );
- bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());
+ THEORY_PROOF(d_bvp = bvp; bvp->attachToSatSolver(*d_satSolver);
+ prop::SatVariable t = d_satSolver->trueVar();
+ prop::SatVariable f = d_satSolver->falseVar();
+ bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f));
}
void TLazyBitblaster::clearSolver() {
* constants to equivalence classes that don't already have them
*/
bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setProofLog(proof::ResolutionBitVectorProof* bvp);
+ void setProofLog(proof::BitVectorProof* bvp);
typedef TNodeSet::const_iterator vars_iterator;
vars_iterator beginVars() { return d_variables.begin(); }
};
TheoryBV* d_bv;
- proof::ResolutionBitVectorProof* d_bvp;
context::Context* d_ctx;
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
- std::unique_ptr<context::Context> d_nullContext;
- // sat solver used for bitblasting and associated CnfStream
std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
- std::unique_ptr<prop::CnfStream> d_cnfStream;
AssertionList*
d_assertedAtoms; /**< context dependent list storing the atoms
void addAtom(TNode atom);
bool hasValue(TNode a);
Node getModelFromSatSolver(TNode a, bool fullModel) override;
+ prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
class Statistics
{
} else {
d_bitblaster.reset(new EagerBitblaster(d_bv, d_context));
THEORY_PROOF(if (d_bvp) {
- d_bitblaster->setResolutionProofLog(d_bvp);
+ d_bitblaster->setProofLog(d_bvp);
d_bvp->setBitblaster(d_bitblaster.get());
});
}
return d_bitblaster->collectModelInfo(m, fullModel);
}
-void EagerBitblastSolver::setResolutionProofLog(
- proof::ResolutionBitVectorProof* bvp)
+void EagerBitblastSolver::setProofLog(proof::BitVectorProof* bvp)
{
d_bvp = bvp;
}
bool isInitialized();
void initialize();
bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
- void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+ void setProofLog(proof::BitVectorProof* bvp);
private:
context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
bool d_useAig;
TheoryBV* d_bv;
- proof::ResolutionBitVectorProof* d_bvp;
+ proof::BitVectorProof* d_bvp;
}; // class EagerBitblastSolver
} // namespace bv
namespace CVC4 {
namespace proof {
-class ResolutionBitVectorProof;
+class BitVectorProof;
}
namespace theory {
return res;
}
virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
- virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+ virtual void setProofLog(proof::BitVectorProof* bvp) {}
AssertionQueue::const_iterator assertionsBegin() {
return d_assertionQueue.begin();
}
d_bv->setConflict(final_conflict);
}
-void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* bvp)
+void BitblastSolver::setProofLog(proof::BitVectorProof* bvp)
{
d_bitblaster->setProofLog( bvp );
bvp->setBitblaster(d_bitblaster.get());
void bitblastQueue();
void setAbstraction(AbstractionModule* module);
uint64_t computeAtomWeight(TNode atom);
- void setProofLog(proof::ResolutionBitVectorProof* bvp) override;
+ void setProofLog(proof::BitVectorProof* bvp) override;
};
} /* namespace CVC4::theory::bv */
return changed;
}
-void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp)
+void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
{
if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
- d_eagerSolver->setResolutionProofLog(bvp);
+ d_eagerSolver->setProofLog(bvp);
}else{
for( unsigned i=0; i< d_subtheories.size(); i++ ){
d_subtheories[i]->setProofLog( bvp );
#include "util/hash.h"
#include "util/statistics_registry.h"
+// Forward declarations, needed because the BV theory and the BV Proof classes
+// are cyclically dependent
+namespace CVC4 {
+namespace proof {
+class BitVectorProof;
+}
+} // namespace CVC4
+
namespace CVC4 {
namespace theory {
namespace bv {
bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+ void setProofLog(proof::BitVectorProof* bvp);
private:
projects / cvc5.git / commitdiff