blob: bbaffabb09c32bad59877e5e1cb18da0f3f6e510 (
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
|
/********************* -*- 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_H
#define __CVC4_H
#include <vector>
#include "cvc4_expr.h"
#include "util/command.h"
#include "util/result.h"
#include "util/model.h"
namespace CVC4 {
class SmtEngine {
/** Current set of assertions. */
// TODO: make context-aware to handle user-level push/pop.
std::vector<Expr> d_assertList;
/** Our expression manager */
ExprManager *d_em;
/** User-level options */
Options *opts;
/**
* 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 ?).
*/
void 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*, Options*) throw();
/**
* 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);
/**
* 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_H */
|
