blob: dffc9905304d99dc96a6d2c8904f98cb7317107e (
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
|
/********************* */
/** theory.h
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 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.
**
** Base of the theory interface.
**/
#ifndef __CVC4__THEORY__THEORY_H
#define __CVC4__THEORY__THEORY_H
#include "expr/node.h"
#include "theory/output_channel.h"
#include "context/context.h"
namespace CVC4 {
namespace theory {
/**
* Base class for T-solvers. Abstract DPLL(T).
*/
class Theory {
/**
* Return whether a node is shared or not. Used by setup().
*/
bool isShared(const Node& n);
public:
/**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
* equality with one of these values (e.g. if STANDARD xxx) but
* rather use range checks (or use the helper functions below).
* Normally we call QUICK_CHECK or STANDARD; at the leaves we call
* with MAX_EFFORT.
*/
enum Effort {
MIN_EFFORT = 0,
QUICK_CHECK = 10,
STANDARD = 50,
FULL_EFFORT = 100
};/* enum Effort */
// TODO add compiler annotation "constant function" here
static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; }
static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; }
static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; }
static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; }
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
* Construct a Theory.
*/
Theory() {
}
/**
* Destructs a Theory. This implementation does nothing, but we
* need a virtual destructor for safety in case subclasses have a
* destructor.
*/
virtual ~Theory() {
}
/**
* Prepare for a Node.
*
* When get() is called to get the next thing off the theory queue,
* setup() is called on its subterms (in TheoryEngine). Then setup()
* is called on this node.
*
* This is done in a "context escape" -- that is, at context level 0.
* setup() MUST NOT MODIFY context-dependent objects that it hasn't
* itself just created.
*/
virtual void setup(const Node& n) = 0;
/**
* Assert a fact in the current context.
*/
void assertFact(const Node& n);
/**
* Check the current assignment's consistency.
*/
virtual void check(OutputChannel& out,
Effort level = FULL_EFFORT) = 0;
/**
* T-propagate new literal assignments in the current context.
*/
virtual void propagate(OutputChannel& out,
Effort level = FULL_EFFORT) = 0;
/**
* Return an explanation for the literal represented by parameter n
* (which was previously propagated by this theory). Report
* explanations to an output channel.
*/
virtual void explain(OutputChannel& out,
const Node& n,
Effort level = FULL_EFFORT) = 0;
protected:
/**
* Returns the next atom in the assertFact() queue.
* Guarentees that registerTerm is called on the theory specific subterms.
* @return the next atom in the assertFact() queue.
*/
Node get();
/**
* Returns true if the assertFactQueue is empty
*/
bool done() { return true; }
};/* class Theory */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__THEORY_H */
|
