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