blob: 02bc0784719f0a05f5c138f696a41f06396d32b5 (
plain)
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
|
/********************* */
/*! \file proof_manager.h
** \verbatim
** Original author: Liana Hadarean
** Major contributors: none
** Minor contributors (to current version): Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief A manager for Proofs
**
** A manager for Proofs.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PROOF_MANAGER_H
#define __CVC4__PROOF_MANAGER_H
#include <iostream>
#include "proof/proof.h"
#include "util/proof.h"
// forward declarations
namespace Minisat {
class Solver;
}/* Minisat namespace */
namespace CVC4 {
namespace prop {
class CnfStream;
}/* CVC4::prop namespace */
class SmtEngine;
typedef int ClauseId;
class Proof;
class SatProof;
class CnfProof;
class TheoryProof;
class LFSCSatProof;
class LFSCCnfProof;
class LFSCTheoryProof;
namespace prop {
typedef uint64_t SatVariable;
class SatLiteral;
typedef std::vector<SatLiteral> SatClause;
}/* CVC4::prop namespace */
// different proof modes
enum ProofFormat {
LFSC,
NATIVE
};/* enum ProofFormat */
std::string append(const std::string& str, uint64_t num);
typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
typedef int ClauseId;
enum ClauseKind {
INPUT,
THEORY_LEMMA,
LEARNT
};/* enum ClauseKind */
class ProofManager {
SatProof* d_satProof;
CnfProof* d_cnfProof;
TheoryProof* d_theoryProof;
// information that will need to be shared across proofs
IdToClause d_inputClauses;
IdToClause d_theoryLemmas;
ExprSet d_inputFormulas;
VarSet d_propVars;
Proof* d_fullProof;
ProofFormat d_format; // used for now only in debug builds
protected:
std::string d_logic;
public:
ProofManager(ProofFormat format = LFSC);
~ProofManager();
static ProofManager* currentPM();
// initialization
static void initSatProof(Minisat::Solver* solver);
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
static void initTheoryProof();
static Proof* getProof(SmtEngine* smt);
static SatProof* getSatProof();
static CnfProof* getCnfProof();
static TheoryProof* getTheoryProof();
// iterators over data shared by proofs
typedef IdToClause::const_iterator clause_iterator;
typedef ExprSet::const_iterator assertions_iterator;
typedef VarSet::const_iterator var_iterator;
clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
var_iterator begin_vars() const { return d_propVars.begin(); }
var_iterator end_vars() const { return d_propVars.end(); }
void addAssertion(Expr formula);
void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
// variable prefixes
static std::string getInputClauseName(ClauseId id);
static std::string getLemmaClauseName(ClauseId id);
static std::string getLearntClauseName(ClauseId id);
static std::string getVarName(prop::SatVariable var);
static std::string getAtomName(prop::SatVariable var);
static std::string getLitName(prop::SatLiteral lit);
void setLogic(const std::string& logic_string);
const std::string getLogic() const { return d_logic; }
};/* class ProofManager */
class LFSCProof : public Proof {
LFSCSatProof* d_satProof;
LFSCCnfProof* d_cnfProof;
LFSCTheoryProof* d_theoryProof;
SmtEngine* d_smtEngine;
public:
LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
virtual void toStream(std::ostream& out);
virtual ~LFSCProof() {}
};/* class LFSCProof */
}/* CVC4 namespace */
#endif /* __CVC4__PROOF_MANAGER_H */
|
