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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
/********************* */
/*! \file bitvector_proof.h
** \verbatim
** Top contributors (to current version):
** Liana Hadarean, Guy Katz, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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__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;
typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
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);
std::map<Expr,std::string> d_constantLetMap;
bool d_useConstantLetification;
context::Context d_fakeContext;
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, bool swap) = 0;
virtual void printAtomBitblastingToFalse(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, ProofLetMap& letMap) = 0;
virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
virtual void calculateAtomsInBitblastingProof() = 0;
};
class LFSCBitVectorProof: public BitVectorProof {
void printConstant(Expr term, std::ostream& os);
void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map);
void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
ExprToString d_exprToVariableName;
ExprToString d_assignedAliases;
std::map<std::string, std::string> d_aliasToBindDeclaration;
std::string assignAlias(Expr expr);
bool hasAlias(Expr expr);
std::set<Node> d_atomsInBitblastingProof;
public:
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
{}
virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
virtual void printTermBitblasting(Expr term, std::ostream& os);
virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
virtual void printBitblasting(std::ostream& os, std::ostream& paren);
virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
void calculateAtomsInBitblastingProof();
const std::set<Node>* getAtomsInBitblastingProof();
void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
};
}/* CVC4 namespace */
#endif /* __CVC4__BITVECTOR__PROOF_H */
|
