diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-03 11:56:47 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-03 11:56:47 -0800 |
commit | aa0a875dfd40bd9dfa810238327db51498b74677 (patch) | |
tree | 5606b1214ef8388b86e964213ed3b9c67254317f /src/proof/bitvector_proof.h | |
parent | 2a19474cdb6761fd4c9aeb0165e661c531ba3e38 (diff) |
Bit vector proof superclass (#2599)
* Split BitvectorProof into a sub/superclass
The superclass contains general printing knowledge.
The subclass contains CNF or Resolution-specific knowledge.
* Renames & code moves
* Nits cleaned in prep for PR
* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof
Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.
* Unique pointers, comments, and code movement.
Adjusted the distribution of code between BVP and RBVP.
Notably, put the CNF proof in BVP because it isn't
resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
BVP's pointer to a CNF proof
RBVP's pointer to a resolution proof
BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`
* clang-format
* Undo manual copyright modification
* s/superclass/base class/
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public
* Andres's Comments
Mostly cleaning up (or trying to clean up) includes.
* Cleaned up one header cycle
However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.
* Added single _s to header gaurds
* Fix Class name in debug output
Credits to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original ordering
Diffstat (limited to 'src/proof/bitvector_proof.h')
-rw-r--r-- | src/proof/bitvector_proof.h | 219 |
1 files changed, 126 insertions, 93 deletions
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 63f1cdf63..466efa6a7 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -9,118 +9,166 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Bitvector proof + ** \brief Bitvector proof base class ** - ** Bitvector proof + ** Contains code (e.g. proof printing code) which is common to all bitvector + *proofs. **/ #include "cvc4_private.h" -#ifndef __CVC4__BITVECTOR__PROOF_H -#define __CVC4__BITVECTOR__PROOF_H +#ifndef __CVC4__BITVECTOR_PROOF_H +#define __CVC4__BITVECTOR_PROOF_H -#include <iostream> #include <set> -#include <sstream> #include <unordered_map> #include <unordered_set> #include <vector> - #include "expr/expr.h" +#include "proof/cnf_proof.h" #include "proof/theory_proof.h" -#include "prop/bvminisat/core/Solver.h" - +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" namespace CVC4 { -namespace prop { -class CnfStream; -} /* namespace CVC4::prop */ - -namespace theory { -namespace bv { -class TheoryBV; -template <class T> class TBitblaster; -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ - -class CnfProof; -} /* namespace CVC4 */ - -namespace CVC4 { - -template <class Solver> class TSatProof; -typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; - typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId; typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr; typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString; -class BitVectorProof : public TheoryProof { -protected: +/** + * A bitvector proof is best understood as having + * + * 1. A declaration of a "bitblasted formulas" -- boolean formulas + * that are each translations of a BV-literal (a comparison between BVs). + * + * (and a proof that each "bitblasted formula" is implied by the + * corresponding BV literal) + * + * 2. A declaration of a cnf formula equisatisfiable to the bitblasted + * formula + * + * (and a proof that each clause is implied by some bitblasted formula) + * + * 3. A proof of UNSAT from the clauses. + * + * This class is responsible for 1 & 2. The proof of UNSAT is delegated to a + * subclass. + */ +class BitVectorProof : public TheoryProof +{ + protected: + BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); + virtual ~BitVectorProof(){}; + + // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ]) ExprSet d_declarations; - ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof + // terms and formulas that are actually relevant to the proof + ExprSet d_usedBB; + + ExprSet d_seenBBTerms; // terms that need to be bit-blasted + std::vector<Expr> d_bbTerms; // order of bit-blasting - ExprSet d_seenBBTerms; // terms that need to be bit-blasted - std::vector<Expr> d_bbTerms; // order of bit-blasting - ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted + /** atoms that need to be bit-blasted, + * BV-literals -> (BV-literals <=> bool formula) + * where a BV literal is a signed or unsigned comparison. + */ + ExprToExpr d_bbAtoms; // map from Expr representing normalized lemma to ClauseId in SAT solver ExprToClauseId d_bbConflictMap; - BVSatProof* d_resolutionProof; - CnfProof* d_cnfProof; - - bool d_isAssumptionConflict; theory::bv::TBitblaster<Node>* d_bitblaster; + + /** In an LFSC proof the manifestation of this expression bit-level + * representation will have a string name. This method returns that name. + */ std::string getBBTermName(Expr expr); - std::map<Expr,std::string> d_constantLetMap; + /** A mapping from constant BV terms to identifiers that will refer to them in + * an LFSC proof, if constant-letification is enabled. + */ + std::map<Expr, std::string> d_constantLetMap; + + /** Should we introduced identifiers to refer to BV constant terms? It may + * reduce the textual size of a proof! + */ bool d_useConstantLetification; - theory::TheoryId getTheoryId() override; - context::Context d_fakeContext; -public: - BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); - void initSatProof(CVC4::BVMinisat::Solver* solver); - void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - void setBitblaster(theory::bv::TBitblaster<Node>* bb); + /** Temporary storage for the set of nodes in the bitblasted formula which + * correspond to CNF variables eventually used in the proof of unsat on the + * CNF formula + */ + std::set<Node> d_atomsInBitblastingProof; - BVSatProof* getSatProof(); - CnfProof* getCnfProof() {return d_cnfProof; } - void finalizeConflicts(std::vector<Expr>& conflicts); + /** + * Prints out + * (a) a declaration of bit-level interpretations corresponding to bits in + * the input BV terms. + * (b) a proof that the each BV literal entails a boolean formula on + * bitof expressions. + */ + void printBitblasting(std::ostream& os, std::ostream& paren); - void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); - void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); /** - * All the - * - * @param confl an inconsistent set of bv literals + * The proof that the bit-blasted SAT formula is correctly converted to CNF */ - void endBVConflict(const BVMinisat::Solver::TLitVec& confl); - void markAssumptionConflict() { d_isAssumptionConflict = true; } - bool isAssumptionConflict() { return d_isAssumptionConflict; } + std::unique_ptr<CnfProof> d_cnfProof; + + public: + void printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; + + void printOwnedSort(Type type, std::ostream& os) override; + + /** + * Populate the d_atomsInBitblastingProof member. + * See its documentation + */ + virtual void calculateAtomsInBitblastingProof() = 0; + + /** + * Read the d_atomsInBitblastingProof member. + * See its documentation. + */ + const std::set<Node>* getAtomsInBitblastingProof(); void registerTermBB(Expr term); + + /** + * Informs the proof that the `atom` predicate was bitblasted into the + * `atom_bb` term. + * + * The `atom` term must be a comparison of bitvectors, and the `atom_bb` term + * a boolean formula on bitof expressions + */ void registerAtomBB(Expr atom, Expr atom_bb); void registerTerm(Expr term) override; - virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; + /** + * This must be done before registering any terms or atoms, since the CNF + * proof must reflect the result of bitblasting those + */ + virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; - virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0; - virtual const std::set<Node>* getAtomsInBitblastingProof() = 0; - virtual void calculateAtomsInBitblastingProof() = 0; -}; + CnfProof* getCnfProof() { return d_cnfProof.get(); } + + void setBitblaster(theory::bv::TBitblaster<Node>* bb); -class LFSCBitVectorProof: public BitVectorProof { + private: + ExprToString d_exprToVariableName; + + ExprToString d_assignedAliases; + std::map<std::string, std::string> d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); + // Functions for printing various BV terms. Helpers for BV's `printOwnedTerm` void printConstant(Expr term, std::ostream& os); void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map); void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map); @@ -128,29 +176,19 @@ class LFSCBitVectorProof: public BitVectorProof { void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map); void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map); - ExprToString d_exprToVariableName; - ExprToString d_assignedAliases; - std::map<std::string, std::string> d_aliasToBindDeclaration; - std::string assignAlias(Expr expr); - bool hasAlias(Expr expr); + /** + * Prints the LFSC construction of a bblast_term for `term` + */ + void printTermBitblasting(Expr term, std::ostream& os); - std::set<Node> d_atomsInBitblastingProof; + /** + * For a given BV-atom (a comparison), prints a proof that that comparison + * holds iff the bitblasted equivalent of it holds. + * Uses a side-condidition to do the bit-blasting. + */ + void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + void printAtomBitblastingToFalse(Expr term, std::ostream& os); -public: - LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - :BitVectorProof(bv, proofEngine) - {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; - void printOwnedSort(Type type, std::ostream& os) override; - void printTermBitblasting(Expr term, std::ostream& os) override; - void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override; - void printAtomBitblastingToFalse(Expr term, std::ostream& os) override; - void printTheoryLemmaProof(std::vector<Expr>& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) override; void printSortDeclarations(std::ostream& os, std::ostream& paren) override; void printTermDeclarations(std::ostream& os, std::ostream& paren) override; void printDeferredDeclarations(std::ostream& os, @@ -158,12 +196,7 @@ public: void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap& globalLetMap) override; - void printBitblasting(std::ostream& os, std::ostream& paren) override; - void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) override; - void calculateAtomsInBitblastingProof() override; - const std::set<Node>* getAtomsInBitblastingProof() override; + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, |