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
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Morgan Deters, Dejan Jovanovic
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* A "valuation" proxy for TheoryEngine
*
* A "valuation" proxy for TheoryEngine. This class breaks the dependence
* of theories' getValue() implementations on TheoryEngine. getValue()
* takes a Valuation, which delegates to TheoryEngine.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__VALUATION_H
#define CVC5__THEORY__VALUATION_H
#include "context/cdlist.h"
#include "expr/node.h"
#include "options/theory_options.h"
namespace cvc5 {
class TheoryEngine;
namespace theory {
struct Assertion;
class TheoryModel;
class SortInference;
/**
* The status of an equality in the current context.
*/
enum EqualityStatus {
/** The equality is known to be true and has been propagated */
EQUALITY_TRUE_AND_PROPAGATED,
/** The equality is known to be false and has been propagated */
EQUALITY_FALSE_AND_PROPAGATED,
/** The equality is known to be true */
EQUALITY_TRUE,
/** The equality is known to be false */
EQUALITY_FALSE,
/** The equality is not known, but is true in the current model */
EQUALITY_TRUE_IN_MODEL,
/** The equality is not known, but is false in the current model */
EQUALITY_FALSE_IN_MODEL,
/** The equality is completely unknown */
EQUALITY_UNKNOWN
};/* enum EqualityStatus */
std::ostream& operator<<(std::ostream& os, EqualityStatus s);
/**
* Returns true if the two statuses are compatible, i.e. both TRUE
* or both FALSE (regardless of inmodel/propagation).
*/
bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
class Valuation {
TheoryEngine* d_engine;
public:
Valuation(TheoryEngine* engine) :
d_engine(engine) {
}
/**
* Return true if n has an associated SAT literal
*/
bool isSatLiteral(TNode n) const;
/**
* Get the current SAT assignment to the node n.
*
* This is only permitted if n is a theory atom that has an associated
* SAT literal (or its negation).
*
* @return Node::null() if no current assignment; otherwise true or false.
*/
Node getSatValue(TNode n) const;
/**
* Returns true if the node has a current SAT assignment. If yes, the
* argument "value" is set to its value.
*
* This is only permitted if n is a theory atom that has an associated
* SAT literal.
*
* @return true if the literal has a current assignment, and returns the
* value in the "value" argument; otherwise false and the "value"
* argument is unmodified.
*/
bool hasSatValue(TNode n, bool& value) const;
/**
* Returns the equality status of the two terms, from the theory that owns the domain type.
* The types of a and b must be the same.
*/
EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Returns the model value of the shared term (or null if not available).
*/
Node getModelValue(TNode var);
/**
* Returns pointer to model. This model is only valid during last call effort
* check.
*/
TheoryModel* getModel();
/**
* Returns a pointer to the sort inference module, which lives in TheoryEngine
* and is non-null when options::sortInference is true.
*/
SortInference* getSortInference();
//-------------------------------------- static configuration of the model
/**
* Set that k is an unevaluated kind in the TheoryModel, if it exists.
* See TheoryModel::setUnevaluatedKind for details.
*/
void setUnevaluatedKind(Kind k);
/**
* Set that k is an unevaluated kind in the TheoryModel, if it exists.
* See TheoryModel::setSemiEvaluatedKind for details.
*/
void setSemiEvaluatedKind(Kind k);
/**
* Set that k is an irrelevant kind in the TheoryModel, if it exists.
* See TheoryModel::setIrrelevantKind for details.
*/
void setIrrelevantKind(Kind k);
//-------------------------------------- end static configuration of the model
/**
* Ensure that the given node will have a designated SAT literal
* that is definitionally equal to it. The result of this function
* is a Node that can be queried via getSatValue().
*
* Note that this call may add lemmas to the SAT solver corresponding to the
* definition of subterms eliminated by preprocessing.
*
* @return the actual node that's been "literalized," which may
* differ from the input due to theory-rewriting and preprocessing,
* as well as CNF conversion
*/
CVC5_WARN_UNUSED_RESULT Node ensureLiteral(TNode n);
/**
* This returns the theory-preprocessed form of term n. The theory
* preprocessed form of a term t is one returned by
* TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In
* particular, the returned term has syntax sugar symbols eliminated
* (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE
* terms eliminated) and has been rewritten.
*
* Note that this call may add lemmas to the SAT solver corresponding to the
* definition of subterms eliminated by preprocessing.
*
* @param n The node to preprocess
* @return The preprocessed form of n
*/
Node getPreprocessedTerm(TNode n);
/**
* Same as above, but also tracks the skolems and their corresponding
* definitions in sks and skAsserts respectively.
*/
Node getPreprocessedTerm(TNode n,
std::vector<Node>& skAsserts,
std::vector<Node>& sks);
/**
* Returns whether the given lit (which must be a SAT literal) is a decision
* literal or not. Throws an exception if lit is not a SAT literal. "lit" may
* be in either phase; that is, if "lit" is a SAT literal, this function returns
* true both for lit and the negation of lit.
*/
bool isDecision(Node lit) const;
/**
* Return SAT context level at which `lit` was decided on.
*
* @param lit: The node in question, must have an associated SAT literal.
* @return Decision level of the SAT variable of `lit` (phase is disregarded),
* or -1 if `lit` has not been assigned yet.
*/
int32_t getDecisionLevel(Node lit) const;
/**
* Return the user-context level when `lit` was introduced..
*
* @return User-context level or -1 if not yet introduced.
*/
int32_t getIntroLevel(Node lit) const;
/**
* Get the assertion level of the SAT solver.
*/
unsigned getAssertionLevel() const;
/**
* Request an entailment check according to the given theoryOfMode.
* See theory.h for documentation on entailmentCheck().
*/
std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
/** need check ? */
bool needCheck() const;
/**
* Is the literal lit (possibly) critical for satisfying the input formula in
* the current context? This call is applicable only during collectModelInfo
* or during LAST_CALL effort.
*/
bool isRelevant(Node lit) const;
//------------------------------------------- access methods for assertions
/**
* The following methods are intended only to be used in limited use cases,
* for cases where a theory (e.g. quantifiers) requires knowing about the
* assertions from other theories.
*/
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
/** The beginning iterator of facts for theory tid.*/
context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
};/* class Valuation */
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__VALUATION_H */
|
