1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief A "valuation" proxy for TheoryEngine
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.
19 #include "cvc4_private.h"
21 #ifndef CVC4__THEORY__VALUATION_H
22 #define CVC4__THEORY__VALUATION_H
24 #include "expr/node.h"
25 #include "options/theory_options.h"
36 * The status of an equality in the current context.
39 /** The equality is known to be true and has been propagated */
40 EQUALITY_TRUE_AND_PROPAGATED
,
41 /** The equality is known to be false and has been propagated */
42 EQUALITY_FALSE_AND_PROPAGATED
,
43 /** The equality is known to be true */
45 /** The equality is known to be false */
47 /** The equality is not known, but is true in the current model */
48 EQUALITY_TRUE_IN_MODEL
,
49 /** The equality is not known, but is false in the current model */
50 EQUALITY_FALSE_IN_MODEL
,
51 /** The equality is completely unknown */
53 };/* enum EqualityStatus */
55 std::ostream
& operator<<(std::ostream
& os
, EqualityStatus s
);
58 * Returns true if the two statuses are compatible, i.e. both TRUE
59 * or both FALSE (regardless of inmodel/propagation).
61 bool equalityStatusCompatible(EqualityStatus s1
, EqualityStatus s2
);
64 TheoryEngine
* d_engine
;
66 Valuation(TheoryEngine
* engine
) :
71 * Return true if n has an associated SAT literal
73 bool isSatLiteral(TNode n
) const;
76 * Get the current SAT assignment to the node n.
78 * This is only permitted if n is a theory atom that has an associated
79 * SAT literal (or its negation).
81 * @return Node::null() if no current assignment; otherwise true or false.
83 Node
getSatValue(TNode n
) const;
86 * Returns true if the node has a current SAT assignment. If yes, the
87 * argument "value" is set to its value.
89 * This is only permitted if n is a theory atom that has an associated
92 * @return true if the literal has a current assignment, and returns the
93 * value in the "value" argument; otherwise false and the "value"
94 * argument is unmodified.
96 bool hasSatValue(TNode n
, bool& value
) const;
99 * Returns the equality status of the two terms, from the theory that owns the domain type.
100 * The types of a and b must be the same.
102 EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
105 * Returns the model value of the shared term (or null if not available).
107 Node
getModelValue(TNode var
);
110 * Returns pointer to model. This model is only valid during last call effort
113 TheoryModel
* getModel();
115 //-------------------------------------- static configuration of the model
117 * Set that k is an unevaluated kind in the TheoryModel, if it exists.
118 * See TheoryModel::setUnevaluatedKind for details.
120 void setUnevaluatedKind(Kind k
);
122 * Set that k is an unevaluated kind in the TheoryModel, if it exists.
123 * See TheoryModel::setSemiEvaluatedKind for details.
125 void setSemiEvaluatedKind(Kind k
);
127 * Set that k is an irrelevant kind in the TheoryModel, if it exists.
128 * See TheoryModel::setIrrelevantKind for details.
130 void setIrrelevantKind(Kind k
);
131 //-------------------------------------- end static configuration of the model
134 * Ensure that the given node will have a designated SAT literal
135 * that is definitionally equal to it. The result of this function
136 * is a Node that can be queried via getSatValue().
138 * @return the actual node that's been "literalized," which may
139 * differ from the input due to theory-rewriting and preprocessing,
140 * as well as CNF conversion
142 Node
ensureLiteral(TNode n
) CVC4_WARN_UNUSED_RESULT
;
145 * Returns whether the given lit (which must be a SAT literal) is a decision
146 * literal or not. Throws an exception if lit is not a SAT literal. "lit" may
147 * be in either phase; that is, if "lit" is a SAT literal, this function returns
148 * true both for lit and the negation of lit.
150 bool isDecision(Node lit
) const;
153 * Get the assertion level of the SAT solver.
155 unsigned getAssertionLevel() const;
158 * Request an entailment check according to the given theoryOfMode.
159 * See theory.h for documentation on entailmentCheck().
161 std::pair
<bool, Node
> entailmentCheck(options::TheoryOfMode mode
, TNode lit
);
164 bool needCheck() const;
167 * Is the literal lit (possibly) critical for satisfying the input formula in
168 * the current context? This call is applicable only during collectModelInfo
169 * or during LAST_CALL effort.
171 bool isRelevant(Node lit
) const;
172 };/* class Valuation */
174 }/* CVC4::theory namespace */
175 }/* CVC4 namespace */
177 #endif /* CVC4__THEORY__VALUATION_H */