src/theory/valuation.h

   1 /*********************                                                        */
   2 /*! \file valuation.h
   3  ** \verbatim
   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
  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
  26 namespace CVC4 {
  27
  28 class TheoryEngine;
  29
  30 namespace theory {
  31
  32 /**
  33  * The status of an equality in the current context.
  34  */
  35 enum EqualityStatus {
  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 */
  41   EQUALITY_TRUE,
  42   /** The equality is known to be false */
  43   EQUALITY_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 */
  49   EQUALITY_UNKNOWN
  50 };
  51
  52 /**
  53  * Returns true if the two statuses are compatible, i.e. bot TRUE
  54  * or both FALSE (regardles of inmodel/propagation).
  55  */
  56 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
  57
  58 class Valuation {
  59   TheoryEngine* d_engine;
  60 public:
  61   Valuation(TheoryEngine* engine) :
  62     d_engine(engine) {
  63   }
  64
  65   /*
  66    * Return true if n has an associated SAT literal
  67    */
  68   bool isSatLiteral(TNode n) const;
  69
  70   /**
  71    * Get the current SAT assignment to the node n.
  72    *
  73    * This is only permitted if n is a theory atom that has an associated
  74    * SAT literal (or its negation).
  75    *
  76    * @return Node::null() if no current assignment; otherwise true or false.
  77    */
  78   Node getSatValue(TNode n) const;
  79
  80   /**
  81    * Returns true if the node has a current SAT assignment. If yes, the
  82    * argument "value" is set to its value.
  83    *
  84    * This is only permitted if n is a theory atom that has an associated
  85    * SAT literal.
  86    *
  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.
  90    */
  91   bool hasSatValue(TNode n, bool& value) const;
  92
  93   /**
  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.
  96    */
  97   EqualityStatus getEqualityStatus(TNode a, TNode b);
  98
  99   /**
 100    * Returns the model value of the shared term (or null if not available).
 101    */
 102   Node getModelValue(TNode var);
 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   /**
 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.
 120    */
 121   bool isDecision(Node lit) const;
 122
 123   /**
 124    * Get the assertion level of the SAT solver.
 125    */
 126   unsigned getAssertionLevel() const;
 127
 128 };/* class Valuation */
 129
 130 }/* CVC4::theory namespace */
 131 }/* CVC4 namespace */
 132
 133 #endif /* __CVC4__THEORY__VALUATION_H */