blob: 98cffb6dec5191224b6f1d1110acaec32d20f079 (
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
/********************* -*- C++ -*- */
/** smt_engine.h
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** SmtEngine: the main public entry point of libcvc4.
**/
#ifndef __CVC4__SMT_ENGINE_H
#define __CVC4__SMT_ENGINE_H
#include <vector>
#include "cvc4_config.h"
#include "expr/node.h"
#include "expr/expr.h"
#include "expr/node_manager.h"
#include "expr/expr_manager.h"
#include "util/result.h"
#include "util/model.h"
#include "util/options.h"
#include "prop/prop_engine.h"
#include "util/decision_engine.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
// PropEngine.
namespace CVC4 {
class Command;
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
// hood): use a type parameter and have check() delegate, or subclass
// SmtEngine and override check()?
//
// Probably better than that is to have a configuration object that
// indicates which passes are desired. The configuration occurs
// elsewhere (and can even occur at runtime). A simple "pass manager"
// of sorts determines check()'s behavior.
//
// The CNF conversion can go on in PropEngine.
class CVC4_PUBLIC SmtEngine {
public:
/**
* Construct an SmtEngine with the given expression manager and user options.
*/
SmtEngine(ExprManager* em, Options* opts) throw();
/**
* Destruct the smt engine.
*/
~SmtEngine();
/**
* Execute a command.
*/
void doCommand(Command*);
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
* literals and conjunction of literals. Returns false iff
* inconsistent.
*/
Result assertFormula(const BoolExpr& e);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
Result query(const BoolExpr& e);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
Result checkSat(const BoolExpr& e);
/**
* Simplify a formula without doing "much" work. Requires assist
* from the SAT Engine.
*/
Expr simplify(const Expr& e);
/**
* Get a (counter)model (only if preceded by a SAT or INVALID query.
*/
Model getModel();
/**
* Push a user-level context.
*/
void push();
/**
* Pop a user-level context. Throws an exception if nothing to pop.
*/
void pop();
private:
/** Current set of assertions. */
// TODO: make context-aware to handle user-level push/pop.
std::vector<Node> d_assertions;
/** Our expression manager */
ExprManager *d_public_em;
/** Out internal expression/node manager */
NodeManager *d_em;
/** User-level options */
Options *d_opts;
/** The decision engine */
DecisionEngine d_de;
/** The decision engine */
TheoryEngine d_te;
/** The propositional engine */
PropEngine d_prop;
/**
* Pre-process an Node. This is expected to be highly-variable,
* with a lot of "source-level configurability" to add multiple
* passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
Node preprocess(const Node& e);
/**
* Adds a formula to the current context.
*/
void addFormula(const Node& e);
/**
* Full check of consistency in current context. Returns true iff
* consistent.
*/
Result check();
/**
* Quick check of consistency in current context: calls
* processAssertionList() then look for inconsistency (based only on
* that).
*/
Result quickCheck();
/**
* Process the assertion list: for literals and conjunctions of
* literals, assert to T-solver.
*/
Node processAssertionList();
};/* class SmtEngine */
}/* CVC4 namespace */
#endif /* __CVC4__SMT_ENGINE_H */
|
