1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Dejan Jovanovic
6 ** Minor contributors (to current version): Tim King, Clark Barrett, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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 "theory/theoryof_mode.h"
33 class EntailmentCheckParameters
;
34 class EntailmentCheckSideEffects
;
37 * The status of an equality in the current context.
40 /** The equality is known to be true and has been propagated */
41 EQUALITY_TRUE_AND_PROPAGATED
,
42 /** The equality is known to be false and has been propagated */
43 EQUALITY_FALSE_AND_PROPAGATED
,
44 /** The equality is known to be true */
46 /** The equality is known to be false */
48 /** The equality is not known, but is true in the current model */
49 EQUALITY_TRUE_IN_MODEL
,
50 /** The equality is not known, but is false in the current model */
51 EQUALITY_FALSE_IN_MODEL
,
52 /** The equality is completely unknown */
54 };/* enum EqualityStatus */
57 * Returns true if the two statuses are compatible, i.e. both TRUE
58 * or both FALSE (regardless of inmodel/propagation).
60 bool equalityStatusCompatible(EqualityStatus s1
, EqualityStatus s2
);
63 TheoryEngine
* d_engine
;
65 Valuation(TheoryEngine
* engine
) :
70 * Return true if n has an associated SAT literal
72 bool isSatLiteral(TNode n
) const;
75 * Get the current SAT assignment to the node n.
77 * This is only permitted if n is a theory atom that has an associated
78 * SAT literal (or its negation).
80 * @return Node::null() if no current assignment; otherwise true or false.
82 Node
getSatValue(TNode n
) const;
85 * Returns true if the node has a current SAT assignment. If yes, the
86 * argument "value" is set to its value.
88 * This is only permitted if n is a theory atom that has an associated
91 * @return true if the literal has a current assignment, and returns the
92 * value in the "value" argument; otherwise false and the "value"
93 * argument is unmodified.
95 bool hasSatValue(TNode n
, bool& value
) const;
98 * Returns the equality status of the two terms, from the theory that owns the domain type.
99 * The types of a and b must be the same.
101 EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
104 * Returns the model value of the shared term (or null if not available).
106 Node
getModelValue(TNode var
);
109 * Ensure that the given node will have a designated SAT literal
110 * that is definitionally equal to it. The result of this function
111 * is a Node that can be queried via getSatValue().
113 * @return the actual node that's been "literalized," which may
114 * differ from the input due to theory-rewriting and preprocessing,
115 * as well as CNF conversion
117 Node
ensureLiteral(TNode n
) CVC4_WARN_UNUSED_RESULT
;
120 * Returns whether the given lit (which must be a SAT literal) is a decision
121 * literal or not. Throws an exception if lit is not a SAT literal. "lit" may
122 * be in either phase; that is, if "lit" is a SAT literal, this function returns
123 * true both for lit and the negation of lit.
125 bool isDecision(Node lit
) const;
128 * Get the assertion level of the SAT solver.
130 unsigned getAssertionLevel() const;
133 * Request an entailment check according to the given theoryOfMode.
134 * See theory.h for documentation on entailmentCheck().
136 std::pair
<bool, Node
> entailmentCheck(theory::TheoryOfMode mode
, TNode lit
, const theory::EntailmentCheckParameters
* params
= NULL
, theory::EntailmentCheckSideEffects
* out
= NULL
);
139 bool needCheck() const;
141 };/* class Valuation */
143 }/* CVC4::theory namespace */
144 }/* CVC4 namespace */
146 #endif /* __CVC4__THEORY__VALUATION_H */