summaryrefslogtreecommitdiff
path: root/src/proof/clausal_bitvector_proof.h
diff options
context:
space:
mode:
authorAlex Ozdemir <aozdemir@hmc.edu>2019-01-14 10:53:31 -0800
committerGitHub <noreply@github.com>2019-01-14 10:53:31 -0800
commit23374b9d7fe9363165c99fbbddfd7591302a3431 (patch)
treeb86973ea904e9d6628b4c8a6da0a4619f8b45d51 /src/proof/clausal_bitvector_proof.h
parent300560dda47178cae18f5f4ad2edb381eabddb30 (diff)
ClausalBitvectorProof (#2786)
* [DRAT] ClausalBitvectorProof Created a class, `ClausalBitvectorProof`, which represents a bitvector proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc) It fits into the `BitvectorProof` class hierarchy like this: ``` BitvectorProof / \ / \ ClausalBitvectorProof ResolutionBitvectorProof ``` This change is a painful one because all of the following BV subsystems referenced ResolutionBitvectorProof (subsequently RBVP) or BitvectorProof (subsequently BVP): * CnfStream * SatSolver (specifically the BvSatSolver) * CnfProof * TheoryProof * TheoryBV * Both bitblasters And in particular, ResolutionBitvectorProof, the CnfStream, and the SatSolvers were tightly coupled. This means that references to and interactions with (R)BVP were pervasive. Nevertheless, an SMT developer must persist. The change summary: * Create a subclass of BVP, called ClausalBitvectorProof, which has most methods stubbed out. * Make a some modifications to BVP and ResolutionBitvectorProof as the natural division of labor between the different classes becomes clear. * Go through all the components in the first list and try to figure out which kind of BVP they should **actually** be interacting with, and how. Make tweaks accordingly. * Add a hook from CryptoMinisat which pipes the produced DRAT proof into the new ClausalBitvectorProof. * Add a debug statement to ClausalBitvectorProof which parses and prints that DRAT proof, for testing purposes. Test: * `make check` to verify that we didn't break any old stuff, including lazy BB, and eager BB when using bvminisat. * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that 1. It crashed with "Unimplemented" 2. Right before that it prints out the (textual) DRAT proof. * Remove 2 unneeded methods * Missed a rename * Typos Thanks Andres! Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Address Andres comments * Reorder members of TBitblaster
Diffstat (limited to 'src/proof/clausal_bitvector_proof.h')
-rw-r--r--src/proof/clausal_bitvector_proof.h97
1 files changed, 97 insertions, 0 deletions
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
new file mode 100644
index 000000000..85e409e0d
--- /dev/null
+++ b/src/proof/clausal_bitvector_proof.h
@@ -0,0 +1,97 @@
+/********************* */
+/*! \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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback