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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
/********************* */
/*! \file output_channel.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): taking, barrett
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 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.\endverbatim
**
** \brief The theory output channel interface
**
** The theory output channel interface.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
#define __CVC4__THEORY__OUTPUT_CHANNEL_H
#include "util/Assert.h"
#include "theory/interrupted.h"
namespace CVC4 {
namespace theory {
/**
* A LemmaStatus, returned from OutputChannel::lemma(), provides information
* about the lemma added. In particular, it contains the T-rewritten lemma
* for inspection and the user-level at which the lemma will reside.
*/
class LemmaStatus {
Node d_rewrittenLemma;
unsigned d_level;
public:
LemmaStatus(TNode rewrittenLemma, unsigned level) :
d_rewrittenLemma(rewrittenLemma),
d_level(level) {
}
/** Get the T-rewritten form of the lemma. */
TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; }
/**
* Get the user-level at which the lemma resides. After this user level
* is popped, the lemma is un-asserted from the SAT layer. This level
* will be 0 if the lemma didn't reach the SAT layer at all.
*/
unsigned getLevel() const throw() { return d_level; }
};/* class LemmaStatus */
/**
* Generic "theory output channel" interface.
*/
class OutputChannel {
/** Disallow copying: private constructor */
OutputChannel(const OutputChannel&) CVC4_UNDEFINED;
/** Disallow assignment: private operator=() */
OutputChannel& operator=(const OutputChannel&) CVC4_UNDEFINED;
public:
/**
* Construct an OutputChannel.
*/
OutputChannel() {
}
/**
* Destructs an OutputChannel. This implementation does nothing,
* but we need a virtual destructor for safety in case subclasses
* have a destructor.
*/
virtual ~OutputChannel() {
}
/**
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
*/
virtual void safePoint() throw(Interrupted, AssertionException) {
}
/**
* Indicate a theory conflict has arisen.
*
* @param n - a conflict at the current decision level. This should
* be an AND-kinded node of literals that are TRUE in the current
* assignment and are in conflict (i.e., at least one must be
* assigned false), or else a literal by itself (in the case of a
* unit conflict) which is assigned TRUE (and T-conflicting) in the
* current assignment.
*/
virtual void conflict(TNode n) throw(AssertionException) = 0;
/**
* Propagate a theory literal.
*
* @param n - a theory consequence at the current decision level
* @return false if an immediate conflict was encountered
*/
virtual bool propagate(TNode n) throw(AssertionException) = 0;
/**
* Request that the core make a decision on this atom. The decision
* will be "as soon as possible," but due to other propagation and
* conflict-detection work going on internally, the request is queued
* up and may be behind other such requests. The request will be
* silently dropped if the atom has a definite value at the point the
* request would be serviced. This request is also context-dependent
* on the search context, meaning that it will be dropped completely
* if a conflict is found before it is serviced. Each request will only
* be serviced a single time, even though the atom may become undefined
* due to backtracking.
*
* @param atom the atom to decide upon (or the negation of an
* atom---the decision will be in the phase provided); must be
* associated to a SAT literal.
*/
virtual void propagateAsDecision(TNode n) throw(AssertionException) = 0;
/**
* Tell the core that a valid theory lemma at decision level 0 has
* been detected. (This requests a split.)
*
* @param n - a theory lemma valid at decision level 0
* @param removable - whether the lemma can be removed at any point
* @return the "status" of the lemma, including user level at which
* the lemma resides; the lemma will be removed when this user level pops
*/
virtual LemmaStatus lemma(TNode n, bool removable = false)
throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
/**
* Request a split on a new theory atom. This is equivalent to
* calling lemma({OR n (NOT n)}).
*
* @param n - a theory atom; must be of Boolean type
*/
LemmaStatus split(TNode n)
throw(TypeCheckingExceptionPrivate, AssertionException) {
return lemma(n.orNode(n.notNode()));
}
/**
* Notification from a theory that it realizes it is incomplete at
* this context level. If SAT is later determined by the
* TheoryEngine, it should actually return an UNKNOWN result.
*/
virtual void setIncomplete() throw(AssertionException) = 0;
/**
* "Spend" a "resource." The meaning is specific to the context in
* which the theory is operating, and may even be ignored. The
* intended meaning is that if the user has set a limit on the "units
* of resource" that can be expended in a search, and that limit is
* exceeded, then the search is terminated. Note that the check for
* termination occurs in the main search loop, so while theories
* should call OutputChannel::spendResource() during particularly
* long-running operations, they cannot rely on resource() to break
* out of infinite or intractable computations.
*/
virtual void spendResource() throw() {
}
};/* class OutputChannel */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */
|
