1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): taking, barrett, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A "valuation" proxy for TheoryEngine
16 ** A "valuation" proxy for TheoryEngine. This class breaks the dependence
17 ** of theories' getValue() implementations on TheoryEngine. getValue()
18 ** takes a Valuation, which delegates to TheoryEngine.
21 #include "cvc4_private.h"
23 #ifndef __CVC4__THEORY__VALUATION_H
24 #define __CVC4__THEORY__VALUATION_H
26 #include "expr/node.h"
27 #include "theory/substitutions.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 */
56 * Returns true if the two statuses are compatible, i.e. bot TRUE
57 * or both FALSE (regardles of inmodel/propagation).
59 bool equalityStatusCompatible(EqualityStatus s1
, EqualityStatus s2
);
62 TheoryEngine
* d_engine
;
64 Valuation(TheoryEngine
* engine
) :
68 Node
getValue(TNode n
) const;
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 * Ensure that the given node will have a designated SAT literal
106 * that is definitionally equal to it. The result of this function
107 * is a Node that can be queried via getSatValue().
109 * @return the actual node that's been "literalized," which may
110 * differ from the input due to theory-rewriting and preprocessing,
111 * as well as CNF conversion
113 Node
ensureLiteral(TNode n
) CVC4_WARN_UNUSED_RESULT
;
115 };/* class Valuation */
117 }/* CVC4::theory namespace */
118 }/* CVC4 namespace */
120 #endif /* __CVC4__THEORY__VALUATION_H */