diff options
Diffstat (limited to 'src/proof/resolution_bitvector_proof.h')
-rw-r--r-- | src/proof/resolution_bitvector_proof.h | 113 |
1 files changed, 0 insertions, 113 deletions
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h deleted file mode 100644 index a1b0b0d59..000000000 --- a/src/proof/resolution_bitvector_proof.h +++ /dev/null @@ -1,113 +0,0 @@ -/********************* */ -/*! \file resolution_bitvector_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Mathias Preiner, Liana Hadarean - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 - ** - ** Bitvector proof - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H -#define CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H - -#include <iosfwd> - -#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 { - -typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof; - -namespace proof { - -/** - * Represents a bitvector proof which is backed by - * (a) bitblasting and - * (b) a resolution unsat proof. - * - * Contains tools for constructing BV conflicts - */ -class ResolutionBitVectorProof : public BitVectorProof -{ - public: - ResolutionBitVectorProof(theory::bv::TheoryBV* bv, - TheoryProofEngine* proofEngine); - - /** - * Create an (internal) SAT proof object - * Must be invoked before manipulating BV conflicts, - * or initializing a BNF proof - */ - void initSatProof(CVC4::BVMinisat::Solver* solver); - - BVSatProof* getSatProof(); - - void finalizeConflicts(std::vector<Expr>& conflicts) override; - - void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); - void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); - void endBVConflict(const BVMinisat::Solver::TLitVec& confl); - - void markAssumptionConflict() { d_isAssumptionConflict = true; } - bool isAssumptionConflict() const { return d_isAssumptionConflict; } - - 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. - // This is that proof. - std::unique_ptr<BVSatProof> d_resolutionProof; - - bool d_isAssumptionConflict; - -}; - -class LfscResolutionBitVectorProof : public ResolutionBitVectorProof -{ - public: - LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv, - TheoryProofEngine* proofEngine) - : ResolutionBitVectorProof(bv, proofEngine) - { - } - 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; - void calculateAtomsInBitblastingProof() override; -}; - -} // namespace proof - -} // namespace CVC4 - -#endif /* CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ |