1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
/********************* */
/*! \file bitvector_proof.h
** \verbatim
** Original author: Liana Hadarean
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** 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__BITVECTOR__PROOF_H
#define __CVC4__BITVECTOR__PROOF_H
//#include <cstdint>
#include <ext/hash_map>
#include <ext/hash_set>
#include <iostream>
#include <set>
#include <sstream>
#include <vector>
#include "expr/expr.h"
#include "proof/theory_proof.h"
#include "prop/bvminisat/core/Solver.h"
namespace CVC4 {
namespace prop {
class CnfStream;
} /* namespace CVC4::prop */
namespace theory {
namespace bv {
class TheoryBV;
template <class T> class TBitblaster;
} /* namespace CVC4::theory::bv */
} /* namespace CVC4::theory */
class CnfProof;
} /* namespace CVC4 */
namespace CVC4 {
template <class Solver> class TSatProof;
typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
template <class Solver> class LFSCSatProof;
typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
class BitVectorProof : public TheoryProof {
protected:
ExprSet d_declarations;
ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof
ExprSet d_seenBBTerms; // terms that need to be bit-blasted
std::vector<Expr> d_bbTerms; // order of bit-blasting
ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted
// map from Expr representing normalized lemma to ClauseId in SAT solver
ExprToClauseId d_bbConflictMap;
BVSatProof* d_resolutionProof;
CnfProof* d_cnfProof;
bool d_isAssumptionConflict;
theory::bv::TBitblaster<Node>* d_bitblaster;
std::string getBBTermName(Expr expr);
public:
BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
void initSatProof(CVC4::BVMinisat::Solver* solver);
void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
void setBitblaster(theory::bv::TBitblaster<Node>* bb);
BVSatProof* getSatProof();
CnfProof* getCnfProof() {return d_cnfProof; }
void finalizeConflicts(std::vector<Expr>& conflicts);
void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
/**
* All the
*
* @param confl an inconsistent set of bv literals
*/
void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
void markAssumptionConflict() { d_isAssumptionConflict = true; }
bool isAssumptionConflict() { return d_isAssumptionConflict; }
void registerTermBB(Expr term);
void registerAtomBB(Expr atom, Expr atom_bb);
virtual void registerTerm(Expr term);
virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0;
virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
};
class LFSCBitVectorProof: public BitVectorProof {
void printConstant(Expr term, std::ostream& os);
void printOperatorNary(Expr term, std::ostream& os, const LetMap& map);
void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map);
void printPredicate(Expr term, std::ostream& os, const LetMap& map);
void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
void printBitOf(Expr term, std::ostream& os);
public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
{}
virtual void printTerm(Expr term, std::ostream& os, const LetMap& map);
virtual void printSort(Type type, std::ostream& os);
virtual void printTermBitblasting(Expr term, std::ostream& os);
virtual void printAtomBitblasting(Expr term, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
virtual void printDeclarations(std::ostream& os, std::ostream& paren);
virtual void printBitblasting(std::ostream& os, std::ostream& paren);
virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
};
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR__PROOF_H */
|
