blob: 3e33cc8af1ce944aa598b21b071dc67524fe88a2 (
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
|
/********************* -*- C++ -*- */
/** cvc4.h
** 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.
**
**/
#ifndef __CVC4__SMT_ENGINE_H
#define __CVC4__SMT_ENGINE_H
#include <vector>
#include "cvc4_config.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/result.h"
#include "util/model.h"
#include "util/options.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 SmtEngine {
/** Current set of assertions. */
// TODO: make context-aware to handle user-level push/pop.
std::vector<Expr> d_assertions;
/** Our expression manager */
ExprManager *d_em;
/** User-level options */
Options *d_opts;
/** Expression built-up for handing off to the propagation engine */
Expr d_expr;
/**
* Pre-process an Expr. This is expected to be highly-variable,
* with a lot of "source-level configurability" to add multiple
* passes over the Expr. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
Expr preprocess(Expr);
/**
* Adds a formula to the current context.
*/
void addFormula(Expr);
/**
* 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.
*/
void processAssertionList();
public:
/*
* Construct an SmtEngine with the given expression manager and user options.
*/
SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {}
/**
* 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 assert(Expr);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
Result query(Expr);
/**
* Add a formula to the current context and call check(). Returns
* true iff consistent.
*/
Result checkSat(Expr);
/**
* Simplify a formula without doing "much" work. Requires assist
* from the SAT Engine.
*/
Expr simplify(Expr);
/**
* 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();
};/* class SmtEngine */
}/* CVC4 namespace */
#endif /* __CVC4__SMT_ENGINE_H */
|
