1 /********************* */
2 /*! \file bitvector_proof.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief Bitvector proof
17 #include "cvc4_private.h"
19 #ifndef __CVC4__BITVECTOR__PROOF_H
20 #define __CVC4__BITVECTOR__PROOF_H
25 #include <unordered_map>
26 #include <unordered_set>
29 #include "expr/expr.h"
30 #include "proof/theory_proof.h"
31 #include "prop/bvminisat/core/Solver.h"
38 } /* namespace CVC4::prop */
43 template <class T
> class TBitblaster
;
44 } /* namespace CVC4::theory::bv */
45 } /* namespace CVC4::theory */
48 } /* namespace CVC4 */
52 template <class Solver
> class TSatProof
;
53 typedef TSatProof
< CVC4::BVMinisat::Solver
> BVSatProof
;
55 template <class Solver
> class LFSCSatProof
;
56 typedef LFSCSatProof
< CVC4::BVMinisat::Solver
> LFSCBVSatProof
;
58 typedef std::unordered_set
<Expr
, ExprHashFunction
> ExprSet
;
59 typedef std::unordered_map
<Expr
, ClauseId
, ExprHashFunction
> ExprToClauseId
;
60 typedef std::unordered_map
<Expr
, unsigned, ExprHashFunction
> ExprToId
;
61 typedef std::unordered_map
<Expr
, Expr
, ExprHashFunction
> ExprToExpr
;
62 typedef std::unordered_map
<Expr
, std::string
, ExprHashFunction
> ExprToString
;
64 class BitVectorProof
: public TheoryProof
{
66 ExprSet d_declarations
;
68 ExprSet d_usedBB
; // terms and formulas that are actually relevant to the proof
70 ExprSet d_seenBBTerms
; // terms that need to be bit-blasted
71 std::vector
<Expr
> d_bbTerms
; // order of bit-blasting
72 ExprToExpr d_bbAtoms
; // atoms that need to be bit-blasted
74 // map from Expr representing normalized lemma to ClauseId in SAT solver
75 ExprToClauseId d_bbConflictMap
;
76 BVSatProof
* d_resolutionProof
;
80 bool d_isAssumptionConflict
;
81 theory::bv::TBitblaster
<Node
>* d_bitblaster
;
82 std::string
getBBTermName(Expr expr
);
84 std::map
<Expr
,std::string
> d_constantLetMap
;
85 bool d_useConstantLetification
;
87 context::Context d_fakeContext
;
89 BitVectorProof(theory::bv::TheoryBV
* bv
, TheoryProofEngine
* proofEngine
);
91 void initSatProof(CVC4::BVMinisat::Solver
* solver
);
92 void initCnfProof(prop::CnfStream
* cnfStream
, context::Context
* ctx
);
93 void setBitblaster(theory::bv::TBitblaster
<Node
>* bb
);
95 BVSatProof
* getSatProof();
96 CnfProof
* getCnfProof() {return d_cnfProof
; }
97 void finalizeConflicts(std::vector
<Expr
>& conflicts
);
99 void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr
);
100 void startBVConflict(CVC4::BVMinisat::Solver::TLit lit
);
104 * @param confl an inconsistent set of bv literals
106 void endBVConflict(const BVMinisat::Solver::TLitVec
& confl
);
107 void markAssumptionConflict() { d_isAssumptionConflict
= true; }
108 bool isAssumptionConflict() { return d_isAssumptionConflict
; }
110 void registerTermBB(Expr term
);
111 void registerAtomBB(Expr atom
, Expr atom_bb
);
113 virtual void registerTerm(Expr term
);
115 virtual void printTermBitblasting(Expr term
, std::ostream
& os
) = 0;
116 virtual void printAtomBitblasting(Expr term
, std::ostream
& os
, bool swap
) = 0;
117 virtual void printAtomBitblastingToFalse(Expr term
, std::ostream
& os
) = 0;
119 virtual void printBitblasting(std::ostream
& os
, std::ostream
& paren
) = 0;
120 virtual void printResolutionProof(std::ostream
& os
, std::ostream
& paren
, ProofLetMap
& letMap
) = 0;
121 virtual const std::set
<Node
>* getAtomsInBitblastingProof() = 0;
122 virtual void calculateAtomsInBitblastingProof() = 0;
125 class LFSCBitVectorProof
: public BitVectorProof
{
127 void printConstant(Expr term
, std::ostream
& os
);
128 void printOperatorNary(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
129 void printOperatorUnary(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
130 void printPredicate(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
131 void printOperatorParametric(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
132 void printBitOf(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
134 ExprToString d_exprToVariableName
;
135 ExprToString d_assignedAliases
;
136 std::map
<std::string
, std::string
> d_aliasToBindDeclaration
;
137 std::string
assignAlias(Expr expr
);
138 bool hasAlias(Expr expr
);
140 std::set
<Node
> d_atomsInBitblastingProof
;
143 LFSCBitVectorProof(theory::bv::TheoryBV
* bv
, TheoryProofEngine
* proofEngine
)
144 :BitVectorProof(bv
, proofEngine
)
146 virtual void printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
147 virtual void printOwnedSort(Type type
, std::ostream
& os
);
148 virtual void printTermBitblasting(Expr term
, std::ostream
& os
);
149 virtual void printAtomBitblasting(Expr term
, std::ostream
& os
, bool swap
);
150 virtual void printAtomBitblastingToFalse(Expr term
, std::ostream
& os
);
151 virtual void printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
);
152 virtual void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
);
153 virtual void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
);
154 virtual void printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
);
155 virtual void printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
);
156 virtual void printBitblasting(std::ostream
& os
, std::ostream
& paren
);
157 virtual void printResolutionProof(std::ostream
& os
, std::ostream
& paren
, ProofLetMap
& letMap
);
158 void calculateAtomsInBitblastingProof();
159 const std::set
<Node
>* getAtomsInBitblastingProof();
160 void printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
);
161 void printRewriteProof(std::ostream
& os
, const Node
&n1
, const Node
&n2
);
164 }/* CVC4 namespace */
166 #endif /* __CVC4__BITVECTOR__PROOF_H */