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
|
/********************* */
/*! \file valuation.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief 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 "cvc4_private.h"
#ifndef CVC4__THEORY__VALUATION_H
#define CVC4__THEORY__VALUATION_H
#include "expr/node.h"
#include "options/theory_options.h"
namespace CVC4 {
class TheoryEngine;
namespace theory {
class EntailmentCheckParameters;
class EntailmentCheckSideEffects;
class TheoryModel;
/**
* 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.
*/
TheoryModel* getModel();
/**
* 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().
*
* @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
*/
Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
/**
* 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;
/**
* 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,
const theory::EntailmentCheckParameters* params = NULL,
theory::EntailmentCheckSideEffects* out = NULL);
/** need check ? */
bool needCheck() const;
};/* class Valuation */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* CVC4__THEORY__VALUATION_H */
|
