1 /*********************                                                        */
2 /*! \file valuation.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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
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 "expr/node.h"
25 #include "options/theoryof_mode.h"
26 
27 namespace CVC4 {
28 
29 class TheoryEngine;
30 
31 namespace theory {
32 
33 class EntailmentCheckParameters;
34 class EntailmentCheckSideEffects;
35 class TheoryModel;
36 
37 /**
38  * The status of an equality in the current context.
39  */
40 enum EqualityStatus {
41   /** The equality is known to be true and has been propagated */
42   EQUALITY_TRUE_AND_PROPAGATED,
43   /** The equality is known to be false and has been propagated */
44   EQUALITY_FALSE_AND_PROPAGATED,
45   /** The equality is known to be true */
46   EQUALITY_TRUE,
47   /** The equality is known to be false */
48   EQUALITY_FALSE,
49   /** The equality is not known, but is true in the current model */
50   EQUALITY_TRUE_IN_MODEL,
51   /** The equality is not known, but is false in the current model */
52   EQUALITY_FALSE_IN_MODEL,
53   /** The equality is completely unknown */
54   EQUALITY_UNKNOWN
55 };/* enum EqualityStatus */
56 
57 std::ostream& operator<<(std::ostream& os, EqualityStatus s);
58 
59 /**
60  * Returns true if the two statuses are compatible, i.e. both TRUE
61  * or both FALSE (regardless of inmodel/propagation).
62  */
63 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
64 
65 class Valuation {
66   TheoryEngine* d_engine;
67 public:
Valuation(TheoryEngine * engine)68   Valuation(TheoryEngine* engine) :
69     d_engine(engine) {
70   }
71 
72   /**
73    * Return true if n has an associated SAT literal
74    */
75   bool isSatLiteral(TNode n) const;
76 
77   /**
78    * Get the current SAT assignment to the node n.
79    *
80    * This is only permitted if n is a theory atom that has an associated
81    * SAT literal (or its negation).
82    *
83    * @return Node::null() if no current assignment; otherwise true or false.
84    */
85   Node getSatValue(TNode n) const;
86 
87   /**
88    * Returns true if the node has a current SAT assignment. If yes, the
89    * argument "value" is set to its value.
90    *
91    * This is only permitted if n is a theory atom that has an associated
92    * SAT literal.
93    *
94    * @return true if the literal has a current assignment, and returns the
95    * value in the "value" argument; otherwise false and the "value"
96    * argument is unmodified.
97    */
98   bool hasSatValue(TNode n, bool& value) const;
99 
100   /**
101    * Returns the equality status of the two terms, from the theory that owns the domain type.
102    * The types of a and b must be the same.
103    */
104   EqualityStatus getEqualityStatus(TNode a, TNode b);
105 
106   /**
107    * Returns the model value of the shared term (or null if not available).
108    */
109   Node getModelValue(TNode var);
110 
111   /**
112    * Returns pointer to model.
113    */
114   TheoryModel* getModel();
115 
116   /**
117    * Ensure that the given node will have a designated SAT literal
118    * that is definitionally equal to it.  The result of this function
119    * is a Node that can be queried via getSatValue().
120    *
121    * @return the actual node that's been "literalized," which may
122    * differ from the input due to theory-rewriting and preprocessing,
123    * as well as CNF conversion
124    */
125   Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
126 
127   /**
128    * Returns whether the given lit (which must be a SAT literal) is a decision
129    * literal or not.  Throws an exception if lit is not a SAT literal.  "lit" may
130    * be in either phase; that is, if "lit" is a SAT literal, this function returns
131    * true both for lit and the negation of lit.
132    */
133   bool isDecision(Node lit) const;
134 
135   /**
136    * Get the assertion level of the SAT solver.
137    */
138   unsigned getAssertionLevel() const;
139 
140   /**
141    * Request an entailment check according to the given theoryOfMode.
142    * See theory.h for documentation on entailmentCheck().
143    */
144   std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
145 
146   /** need check ? */
147   bool needCheck() const;
148 
149 };/* class Valuation */
150 
151 }/* CVC4::theory namespace */
152 }/* CVC4 namespace */
153 
154 #endif /* __CVC4__THEORY__VALUATION_H */
155