src/theory/valuation.cpp

   1 /*********************                                                        */
   2 /*! \file valuation.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
   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  ** Implementation of Valuation class.
  15  **/
  16
  17 #include "theory/valuation.h"
  18
  19 #include "expr/node.h"
  20 #include "options/theory_options.h"
  21 #include "theory/rewriter.h"
  22 #include "theory/theory_engine.h"
  23 #include "theory/theory_model.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 std::ostream& operator<<(std::ostream& os, EqualityStatus s)
  29 {
  30   switch (s)
  31   {
  32     case EQUALITY_TRUE_AND_PROPAGATED:
  33       os << "EQUALITY_TRUE_AND_PROPAGATED";
  34       break;
  35     case EQUALITY_FALSE_AND_PROPAGATED:
  36       os << "EQUALITY_FALSE_AND_PROPAGATED";
  37       break;
  38     case EQUALITY_TRUE: os << "EQUALITY_TRUE"; break;
  39     case EQUALITY_FALSE: os << "EQUALITY_FALSE"; break;
  40     case EQUALITY_TRUE_IN_MODEL: os << "EQUALITY_TRUE_IN_MODEL"; break;
  41     case EQUALITY_FALSE_IN_MODEL: os << "EQUALITY_FALSE_IN_MODEL"; break;
  42     case EQUALITY_UNKNOWN: os << "EQUALITY_UNKNOWN"; break;
  43     default: Unhandled(); break;
  44   }
  45   return os;
  46 }
  47
  48 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
  49   switch (s1) {
  50   case EQUALITY_TRUE:
  51   case EQUALITY_TRUE_IN_MODEL:
  52   case EQUALITY_TRUE_AND_PROPAGATED:
  53     switch (s2) {
  54     case EQUALITY_TRUE:
  55     case EQUALITY_TRUE_IN_MODEL:
  56     case EQUALITY_TRUE_AND_PROPAGATED:
  57       return true;
  58     default:
  59       return false;
  60     }
  61     break;
  62   case EQUALITY_FALSE:
  63   case EQUALITY_FALSE_IN_MODEL:
  64   case EQUALITY_FALSE_AND_PROPAGATED:
  65     switch (s2) {
  66     case EQUALITY_FALSE:
  67     case EQUALITY_FALSE_IN_MODEL:
  68     case EQUALITY_FALSE_AND_PROPAGATED:
  69       return true;
  70     default:
  71       return false;
  72     }
  73     break;
  74   default:
  75     return false;
  76   }
  77 }
  78
  79 bool Valuation::isSatLiteral(TNode n) const {
  80   Assert(d_engine != nullptr);
  81   return d_engine->getPropEngine()->isSatLiteral(n);
  82 }
  83
  84 Node Valuation::getSatValue(TNode n) const {
  85   Assert(d_engine != nullptr);
  86   if(n.getKind() == kind::NOT) {
  87     Node atomRes = d_engine->getPropEngine()->getValue(n[0]);
  88     if(atomRes.getKind() == kind::CONST_BOOLEAN) {
  89       return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>());
  90     } else {
  91       Assert(atomRes.isNull());
  92       return atomRes;
  93     }
  94   } else {
  95     return d_engine->getPropEngine()->getValue(n);
  96   }
  97 }
  98
  99 bool Valuation::hasSatValue(TNode n, bool& value) const {
 100   Assert(d_engine != nullptr);
 101   if (d_engine->getPropEngine()->isSatLiteral(n)) {
 102     return d_engine->getPropEngine()->hasValue(n, value);
 103   } else {
 104     return false;
 105   }
 106 }
 107
 108 EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
 109   Assert(d_engine != nullptr);
 110   return d_engine->getEqualityStatus(a, b);
 111 }
 112
 113 Node Valuation::getModelValue(TNode var) {
 114   Assert(d_engine != nullptr);
 115   return d_engine->getModelValue(var);
 116 }
 117
 118 TheoryModel* Valuation::getModel() {
 119   if (d_engine == nullptr)
 120   {
 121     // no theory engine, thus we don't have a model object
 122     return nullptr;
 123   }
 124   return d_engine->getModel();
 125 }
 126
 127 void Valuation::setUnevaluatedKind(Kind k)
 128 {
 129   TheoryModel* m = getModel();
 130   if (m != nullptr)
 131   {
 132     m->setUnevaluatedKind(k);
 133   }
 134   // If no model is available, this command has no effect. This is the case
 135   // when e.g. calling Theory::finishInit for theories that are using a
 136   // Valuation with no model.
 137 }
 138
 139 void Valuation::setSemiEvaluatedKind(Kind k)
 140 {
 141   TheoryModel* m = getModel();
 142   if (m != nullptr)
 143   {
 144     m->setSemiEvaluatedKind(k);
 145   }
 146 }
 147
 148 void Valuation::setIrrelevantKind(Kind k)
 149 {
 150   TheoryModel* m = getModel();
 151   if (m != nullptr)
 152   {
 153     m->setIrrelevantKind(k);
 154   }
 155 }
 156
 157 Node Valuation::ensureLiteral(TNode n) {
 158   Assert(d_engine != nullptr);
 159   return d_engine->ensureLiteral(n);
 160 }
 161
 162 bool Valuation::isDecision(Node lit) const {
 163   Assert(d_engine != nullptr);
 164   return d_engine->getPropEngine()->isDecision(lit);
 165 }
 166
 167 unsigned Valuation::getAssertionLevel() const{
 168   Assert(d_engine != nullptr);
 169   return d_engine->getPropEngine()->getAssertionLevel();
 170 }
 171
 172 std::pair<bool, Node> Valuation::entailmentCheck(options::TheoryOfMode mode,
 173                                                  TNode lit)
 174 {
 175   Assert(d_engine != nullptr);
 176   return d_engine->entailmentCheck(mode, lit);
 177 }
 178
 179 bool Valuation::needCheck() const{
 180   Assert(d_engine != nullptr);
 181   return d_engine->needCheck();
 182 }
 183
 184 bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); }
 185
 186 }/* CVC4::theory namespace */
 187 }/* CVC4 namespace */