GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/valuation.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file valuation.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A "valuation" proxy for TheoryEngine
13
 **
14
 ** A "valuation" proxy for TheoryEngine.  This class breaks the dependence
15
 ** of theories' getValue() implementations on TheoryEngine.  getValue()
16
 ** takes a Valuation, which delegates to TheoryEngine.
17
 **/
18
19
#include "cvc4_private.h"
20
21
#ifndef CVC4__THEORY__VALUATION_H
22
#define CVC4__THEORY__VALUATION_H
23
24
#include "context/cdlist.h"
25
#include "expr/node.h"
26
#include "options/theory_options.h"
27
28
namespace CVC4 {
29
30
class TheoryEngine;
31
32
namespace theory {
33
34
struct Assertion;
35
class TheoryModel;
36
class SortInference;
37
38
/**
39
 * The status of an equality in the current context.
40
 */
41
enum EqualityStatus {
42
  /** The equality is known to be true and has been propagated */
43
  EQUALITY_TRUE_AND_PROPAGATED,
44
  /** The equality is known to be false and has been propagated */
45
  EQUALITY_FALSE_AND_PROPAGATED,
46
  /** The equality is known to be true */
47
  EQUALITY_TRUE,
48
  /** The equality is known to be false */
49
  EQUALITY_FALSE,
50
  /** The equality is not known, but is true in the current model */
51
  EQUALITY_TRUE_IN_MODEL,
52
  /** The equality is not known, but is false in the current model */
53
  EQUALITY_FALSE_IN_MODEL,
54
  /** The equality is completely unknown */
55
  EQUALITY_UNKNOWN
56
};/* enum EqualityStatus */
57
58
std::ostream& operator<<(std::ostream& os, EqualityStatus s);
59
60
/**
61
 * Returns true if the two statuses are compatible, i.e. both TRUE
62
 * or both FALSE (regardless of inmodel/propagation).
63
 */
64
bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
65
66
class Valuation {
67
  TheoryEngine* d_engine;
68
public:
69
126010
  Valuation(TheoryEngine* engine) :
70
126010
    d_engine(engine) {
71
126010
  }
72
73
  /**
74
   * Return true if n has an associated SAT literal
75
   */
76
  bool isSatLiteral(TNode n) const;
77
78
  /**
79
   * Get the current SAT assignment to the node n.
80
   *
81
   * This is only permitted if n is a theory atom that has an associated
82
   * SAT literal (or its negation).
83
   *
84
   * @return Node::null() if no current assignment; otherwise true or false.
85
   */
86
  Node getSatValue(TNode n) const;
87
88
  /**
89
   * Returns true if the node has a current SAT assignment. If yes, the
90
   * argument "value" is set to its value.
91
   *
92
   * This is only permitted if n is a theory atom that has an associated
93
   * SAT literal.
94
   *
95
   * @return true if the literal has a current assignment, and returns the
96
   * value in the "value" argument; otherwise false and the "value"
97
   * argument is unmodified.
98
   */
99
  bool hasSatValue(TNode n, bool& value) const;
100
101
  /**
102
   * Returns the equality status of the two terms, from the theory that owns the domain type.
103
   * The types of a and b must be the same.
104
   */
105
  EqualityStatus getEqualityStatus(TNode a, TNode b);
106
107
  /**
108
   * Returns the model value of the shared term (or null if not available).
109
   */
110
  Node getModelValue(TNode var);
111
112
  /**
113
   * Returns pointer to model. This model is only valid during last call effort
114
   * check.
115
   */
116
  TheoryModel* getModel();
117
  /**
118
   * Returns a pointer to the sort inference module, which lives in TheoryEngine
119
   * and is non-null when options::sortInference is true.
120
   */
121
  SortInference* getSortInference();
122
123
  //-------------------------------------- static configuration of the model
124
  /**
125
   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
126
   * See TheoryModel::setUnevaluatedKind for details.
127
   */
128
  void setUnevaluatedKind(Kind k);
129
  /**
130
   * Set that k is an unevaluated kind in the TheoryModel, if it exists.
131
   * See TheoryModel::setSemiEvaluatedKind for details.
132
   */
133
  void setSemiEvaluatedKind(Kind k);
134
  /**
135
   * Set that k is an irrelevant kind in the TheoryModel, if it exists.
136
   * See TheoryModel::setIrrelevantKind for details.
137
   */
138
  void setIrrelevantKind(Kind k);
139
  //-------------------------------------- end static configuration of the model
140
141
  /**
142
   * Ensure that the given node will have a designated SAT literal
143
   * that is definitionally equal to it.  The result of this function
144
   * is a Node that can be queried via getSatValue().
145
   *
146
   * Note that this call may add lemmas to the SAT solver corresponding to the
147
   * definition of subterms eliminated by preprocessing.
148
   *
149
   * @return the actual node that's been "literalized," which may
150
   * differ from the input due to theory-rewriting and preprocessing,
151
   * as well as CNF conversion
152
   */
153
  Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
154
155
  /**
156
   * This returns the theory-preprocessed form of term n. The theory
157
   * preprocessed form of a term t is one returned by
158
   * TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In
159
   * particular, the returned term has syntax sugar symbols eliminated
160
   * (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE
161
   * terms eliminated) and has been rewritten.
162
   *
163
   * Note that this call may add lemmas to the SAT solver corresponding to the
164
   * definition of subterms eliminated by preprocessing.
165
   *
166
   * @param n The node to preprocess
167
   * @return The preprocessed form of n
168
   */
169
  Node getPreprocessedTerm(TNode n);
170
  /**
171
   * Same as above, but also tracks the skolems and their corresponding
172
   * definitions in sks and skAsserts respectively.
173
   */
174
  Node getPreprocessedTerm(TNode n,
175
                           std::vector<Node>& skAsserts,
176
                           std::vector<Node>& sks);
177
178
  /**
179
   * Returns whether the given lit (which must be a SAT literal) is a decision
180
   * literal or not.  Throws an exception if lit is not a SAT literal.  "lit" may
181
   * be in either phase; that is, if "lit" is a SAT literal, this function returns
182
   * true both for lit and the negation of lit.
183
   */
184
  bool isDecision(Node lit) const;
185
186
  /**
187
   * Get the assertion level of the SAT solver.
188
   */
189
  unsigned getAssertionLevel() const;
190
191
  /**
192
   * Request an entailment check according to the given theoryOfMode.
193
   * See theory.h for documentation on entailmentCheck().
194
   */
195
  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
196
197
  /** need check ? */
198
  bool needCheck() const;
199
200
  /**
201
   * Is the literal lit (possibly) critical for satisfying the input formula in
202
   * the current context? This call is applicable only during collectModelInfo
203
   * or during LAST_CALL effort.
204
   */
205
  bool isRelevant(Node lit) const;
206
207
  //------------------------------------------- access methods for assertions
208
  /**
209
   * The following methods are intended only to be used in limited use cases,
210
   * for cases where a theory (e.g. quantifiers) requires knowing about the
211
   * assertions from other theories.
212
   */
213
  /** The beginning iterator of facts for theory tid.*/
214
  context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
215
  /** The beginning iterator of facts for theory tid.*/
216
  context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
217
};/* class Valuation */
218
219
}/* CVC4::theory namespace */
220
}/* CVC4 namespace */
221
222
#endif /* CVC4__THEORY__VALUATION_H */