1 /********************* */ 2 /*! \file resolution_bitvector_proof.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Alex Ozdemir, Mathias Preiner, Liana Hadarean 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Bitvector proof 13 ** 14 ** Bitvector proof 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H 20 #define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H 21 22 #include <iosfwd> 23 24 #include "context/context.h" 25 #include "expr/expr.h" 26 #include "proof/bitvector_proof.h" 27 #include "proof/sat_proof.h" 28 #include "proof/theory_proof.h" 29 #include "prop/bvminisat/core/Solver.h" 30 #include "prop/cnf_stream.h" 31 #include "prop/sat_solver_types.h" 32 #include "theory/bv/bitblast/bitblaster.h" 33 #include "theory/bv/theory_bv.h" 34 35 namespace CVC4 { 36 37 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof; 38 39 namespace proof { 40 41 /** 42 * Represents a bitvector proof which is backed by 43 * (a) bitblasting and 44 * (b) a resolution unsat proof. 45 * 46 * Contains tools for constructing BV conflicts 47 */ 48 class ResolutionBitVectorProof : public BitVectorProof 49 { 50 public: 51 ResolutionBitVectorProof(theory::bv::TheoryBV* bv, 52 TheoryProofEngine* proofEngine); 53 54 /** 55 * Create an (internal) SAT proof object 56 * Must be invoked before manipulating BV conflicts, 57 * or initializing a BNF proof 58 */ 59 void initSatProof(CVC4::BVMinisat::Solver* solver); 60 61 BVSatProof* getSatProof(); 62 63 void finalizeConflicts(std::vector<Expr>& conflicts) override; 64 65 void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); 66 void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); 67 void endBVConflict(const BVMinisat::Solver::TLitVec& confl); 68 markAssumptionConflict()69 void markAssumptionConflict() { d_isAssumptionConflict = true; } isAssumptionConflict()70 bool isAssumptionConflict() const { return d_isAssumptionConflict; } 71 72 void initCnfProof(prop::CnfStream* cnfStream, 73 context::Context* cnf, 74 prop::SatVariable trueVar, 75 prop::SatVariable falseVar) override; 76 77 protected: 78 void attachToSatSolver(prop::SatSolver& sat_solver) override; 79 80 context::Context d_fakeContext; 81 82 // The CNF formula that results from bit-blasting will need a proof. 83 // This is that proof. 84 std::unique_ptr<BVSatProof> d_resolutionProof; 85 86 bool d_isAssumptionConflict; 87 88 }; 89 90 class LfscResolutionBitVectorProof : public ResolutionBitVectorProof 91 { 92 public: LfscResolutionBitVectorProof(theory::bv::TheoryBV * bv,TheoryProofEngine * proofEngine)93 LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, 94 TheoryProofEngine* proofEngine) 95 : ResolutionBitVectorProof(bv, proofEngine) 96 { 97 } 98 void printTheoryLemmaProof(std::vector<Expr>& lemma, 99 std::ostream& os, 100 std::ostream& paren, 101 const ProofLetMap& map) override; 102 void printBBDeclarationAndCnf(std::ostream& os, 103 std::ostream& paren, 104 ProofLetMap& letMap) override; 105 void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; 106 void calculateAtomsInBitblastingProof() override; 107 }; 108 109 } // namespace proof 110 111 } // namespace CVC4 112 113 #endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ 114