diff options
Diffstat (limited to 'src/proof/clausal_bitvector_proof.h')
| -rw-r--r-- | src/proof/clausal_bitvector_proof.h | 189 |
1 files changed, 0 insertions, 189 deletions
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h deleted file mode 100644 index 28a53c90c..000000000 --- a/src/proof/clausal_bitvector_proof.h +++ /dev/null @@ -1,189 +0,0 @@ -/********************* */ -/*! \file clausal_bitvector_proof.h - ** \verbatim - ** Top contributors (to current version): - ** Alex Ozdemir, Mathias Preiner - ** 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 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" -#include "util/statistics_registry.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::unordered_map<ClauseId, prop::SatClause> d_clauses{}; - std::vector<ClauseId> d_originalClauseIndices{}; - // Stores the proof recieved from the SAT solver. - std::ostringstream d_binaryDratProof{}; - std::vector<ClauseId> d_coreClauseIndices{}; - - struct DratTranslationStatistics - { - DratTranslationStatistics(); - ~DratTranslationStatistics(); - - // Total time spent doing translation (optimized binary DRAT -> in memory - // target format including IO, postprocessing, etc.) - TimerStat d_totalTime; - // Time that the external tool actually spent - TimerStat d_toolTime; - }; - - DratTranslationStatistics d_dratTranslationStatistics; - - private: - // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list - // of clause actually needed to check that proof (a smaller UNSAT core) - void optimizeDratProof(); - - // Given reference to a SAT clause encoded as a vector of literals, puts the - // literals into a canonical order - static void canonicalizeClause(prop::SatClause& clause); - - struct DratOptimizationStatistics - { - DratOptimizationStatistics(); - ~DratOptimizationStatistics(); - - // Total time spent using drat-trim to optimize the DRAT proof/formula - // (including IO, etc.) - TimerStat d_totalTime; - // Time that drat-trim actually spent optimizing the DRAT proof/formula - TimerStat d_toolTime; - // Time that was spent matching clauses in drat-trim's output to clauses in - // its input - TimerStat d_clauseMatchingTime; - // Bytes in binary DRAT proof before optimization - IntStat d_initialDratSize; - // Bytes in binary DRAT proof after optimization - IntStat d_optimizedDratSize; - // Bytes in textual DIMACS bitblasted formula before optimization - IntStat d_initialFormulaSize; - // Bytes in textual DIMACS bitblasted formula after optimization - IntStat d_optimizedFormulaSize; - }; - - DratOptimizationStatistics d_dratOptimizationStatistics; -}; - -/** - * 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) - { - } - - 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; -}; - -/** - * A DRAT proof for a bit-vector problem - */ -class LfscDratBitVectorProof : public LfscClausalBitVectorProof -{ - public: - LfscDratBitVectorProof(theory::bv::TheoryBV* bv, - TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) - { - } - - void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; -}; - -/** - * An LRAT proof for a bit-vector problem - */ -class LfscLratBitVectorProof : public LfscClausalBitVectorProof -{ - public: - LfscLratBitVectorProof(theory::bv::TheoryBV* bv, - TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) - { - } - - void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; -}; - -/** - * An Extended Resolution proof for a bit-vector problem - */ -class LfscErBitVectorProof : public LfscClausalBitVectorProof -{ - public: - LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - : LfscClausalBitVectorProof(bv, proofEngine) - { - } - - void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override; -}; - -} // namespace proof - -} // namespace CVC4 - -#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */ |