1 /********************* */
4 ** Original author: Morgan Deters <mdeters@cs.nyu.edu>
5 ** Major contributors: Dejan Jovanović <dejan.jovanovic@gmail.com>
6 ** Minor contributors (to current version): Tim King <taking@cs.nyu.edu>, Andrew Reynolds <andrew.j.reynolds@gmail.com>, Clark Barrett <barrett@cs.nyu.edu>, Dejan Jovanović <dejan@cs.nyu.edu>
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 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"
33 * The status of an equality in the current context.
36 /** The equality is known to be true and has been propagated */
37 EQUALITY_TRUE_AND_PROPAGATED
,
38 /** The equality is known to be false and has been propagated */
39 EQUALITY_FALSE_AND_PROPAGATED
,
40 /** The equality is known to be true */
42 /** The equality is known to be false */
44 /** The equality is not known, but is true in the current model */
45 EQUALITY_TRUE_IN_MODEL
,
46 /** The equality is not known, but is false in the current model */
47 EQUALITY_FALSE_IN_MODEL
,
48 /** The equality is completely unknown */
53 * Returns true if the two statuses are compatible, i.e. bot TRUE
54 * or both FALSE (regardles of inmodel/propagation).
56 bool equalityStatusCompatible(EqualityStatus s1
, EqualityStatus s2
);
59 TheoryEngine
* d_engine
;
61 Valuation(TheoryEngine
* engine
) :
66 * Return true if n has an associated SAT literal
68 bool isSatLiteral(TNode n
) const;
71 * Get the current SAT assignment to the node n.
73 * This is only permitted if n is a theory atom that has an associated
74 * SAT literal (or its negation).
76 * @return Node::null() if no current assignment; otherwise true or false.
78 Node
getSatValue(TNode n
) const;
81 * Returns true if the node has a current SAT assignment. If yes, the
82 * argument "value" is set to its value.
84 * This is only permitted if n is a theory atom that has an associated
87 * @return true if the literal has a current assignment, and returns the
88 * value in the "value" argument; otherwise false and the "value"
89 * argument is unmodified.
91 bool hasSatValue(TNode n
, bool& value
) const;
94 * Returns the equality status of the two terms, from the theory that owns the domain type.
95 * The types of a and b must be the same.
97 EqualityStatus
getEqualityStatus(TNode a
, TNode b
);
100 * Returns the model value of the shared term (or null if not available).
102 Node
getModelValue(TNode var
);
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
;
116 * Returns whether the given lit (which must be a SAT literal) is a decision
117 * literal or not. Throws an exception if lit is not a SAT literal. "lit" may
118 * be in either phase; that is, if "lit" is a SAT literal, this function returns
119 * true both for lit and the negation of lit.
121 bool isDecision(Node lit
) const;
124 * Get the assertion level of the SAT solver.
126 unsigned getAssertionLevel() const;
128 };/* class Valuation */
130 }/* CVC4::theory namespace */
131 }/* CVC4 namespace */
133 #endif /* __CVC4__THEORY__VALUATION_H */