src/theory/valuation.h

   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-2020 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/theory_options.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:
  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(
 145       options::TheoryOfMode mode,
 146       TNode lit,
 147       const theory::EntailmentCheckParameters* params = NULL,
 148       theory::EntailmentCheckSideEffects* out = NULL);
 149
 150   /** need check ? */
 151   bool needCheck() const;
 152
 153 };/* class Valuation */
 154
 155 }/* CVC4::theory namespace */
 156 }/* CVC4 namespace */
 157
 158 #endif /* CVC4__THEORY__VALUATION_H */