blob: 0e8f50245383805340ffd33e5fcf99baaf312053 (
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
|
vc.h
/* TODO provide way of querying whether you fall into a fragment /
* returning what fragment you're in */
decision_engine.h
// TODO: design decision: decision engine should be notified of
// propagated lits, and also why(?) (so that it can make decisions
// based on the utility of various theories and various theory
// literals). How? Maybe TheoryEngine has a backdoor into
// DecisionEngine "behind the back" of the PropEngine?
result.h
// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
// but this requires doing the same for Prover and needs discussion.
// TODO: subclass to provide models, etc. This is really just
// intended as a three-valued response code.
expr_builder.h
// TODO: store some flags here and install into attribute map when
// the expr is created? (we'd have to do that since we don't know
// it's hash code yet)
expr_builder.h
/* TODO design: these modify ExprBuilder */
ExprBuilder& operator!() { return notExpr(); }
ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
ExprBuilder& operator||(const Expr& right) { return orExpr(right); }
prover.h
// 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.
prover.h
/** (preprocessing)
* 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 ?).
*/
theory.h
// TODO: these use the current EM (but must be renamed)
// TODO design decision: instead of returning a set of literals
// here, perhaps we have an interface back into the prop engine
// where we assert directly. we might sometimes unknowingly assert
// something clearly inconsistent (esp. in a parallel context).
// This would allow the PropEngine to cancel our further work since
// we're already inconsistent---also could strategize dynamically on
// whether enough theory prop work has occurred.
virtual void propagate(Effort level = FULL_EFFORT) = 0;
could provide a continuation (essentially) to propagate literals.
argument Propagator prop
class Propagator {
PropEngine d_pe;
public:
// may not return due to a longjmp (?) or perhaps an exception
// returns next continuation
Propagator operator()(Literal l);
};
==========================
TODO: add throw() specifications
|
