blob: e48d6336c7970a78a354fa9ad3af12014f562a6b (
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
|
/********************* -*- C++ -*- */
/** prover.h
** This file is part of the CVC4 prototype.
**
** The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
**/
#ifndef __CVC4_PROVER_H
#define __CVC4_PROVER_H
#include <vector>
#include "expr.h"
#include "result.h"
#include "model.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
// PropEngine.
namespace CVC4 {
// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
// hood): use a type parameter and have check() delegate, or subclass
// Prover 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 Prover {
/** Current set of assertions. */
// TODO: make context-aware to handle user-level push/pop.
std::vector<Expr> d_assertList;
private:
/**
* 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:
/**
* 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 Prover */
} /* CVC4 namespace */
#endif /* __CVC4_PROVER_H */
|
