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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 nonnull 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 theoryrewriting and preprocessing, 
151 

* as well as CNF conversion 
152 

*/ 
153 

Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT; 
154 


155 

/** 
156 

* This returns the theorypreprocessed 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 */ 