src/theory/valuation.h

   1 /*********************                                                        */
   2 /*! \file valuation.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief A "valuation" proxy for TheoryEngine
  15  **
  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.
  19  **/
  20
  21 #include "cvc4_private.h"
  22
  23 #ifndef __CVC4__THEORY__VALUATION_H
  24 #define __CVC4__THEORY__VALUATION_H
  25
  26 #include "expr/node.h"
  27 #include "theory/substitutions.h"
  28
  29 namespace CVC4 {
  30
  31 class TheoryEngine;
  32
  33 namespace theory {
  34
  35 /**
  36  * The status of an equality in the current context.
  37  */
  38 enum EqualityStatus {
  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 */
  44   EQUALITY_TRUE,
  45   /** The equality is known to be false */
  46   EQUALITY_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 */
  52   EQUALITY_UNKNOWN
  53 };
  54
  55 /**
  56  * Returns true if the two statuses are compatible, i.e. bot TRUE
  57  * or both FALSE (regardles of inmodel/propagation).
  58  */
  59 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
  60
  61 class Valuation {
  62   TheoryEngine* d_engine;
  63 public:
  64   Valuation(TheoryEngine* engine) :
  65     d_engine(engine) {
  66   }
  67
  68   Node getValue(TNode n) const;
  69
  70   /*
  71    * Return true if n has an associated SAT literal
  72    */
  73   bool isSatLiteral(TNode n) const;
  74
  75   /**
  76    * Get the current SAT assignment to the node n.
  77    *
  78    * This is only permitted if n is a theory atom that has an associated
  79    * SAT literal (or its negation).
  80    *
  81    * @return Node::null() if no current assignment; otherwise true or false.
  82    */
  83   Node getSatValue(TNode n) const;
  84
  85   /**
  86    * Returns true if the node has a current SAT assignment. If yes, the
  87    * argument "value" is set to its value.
  88    *
  89    * This is only permitted if n is a theory atom that has an associated
  90    * SAT literal.
  91    *
  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.
  95    */
  96   bool hasSatValue(TNode n, bool& value) const;
  97
  98   /**
  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.
 101    */
 102   EqualityStatus getEqualityStatus(TNode a, TNode b);
 103
 104   /**
 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().
 108    *
 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
 112    */
 113   Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
 114
 115 };/* class Valuation */
 116
 117 }/* CVC4::theory namespace */
 118 }/* CVC4 namespace */
 119
 120 #endif /* __CVC4__THEORY__VALUATION_H */