src/theory/theory_state.cpp

   1 /*********************                                                        */
   2 /*! \file theory_state.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner
   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 theory state for Theory
  13  **/
  14
  15 #include "theory/theory_state.h"
  16
  17 #include "theory/uf/equality_engine.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21
  22 TheoryState::TheoryState(context::Context* c,
  23                          context::UserContext* u,
  24                          Valuation val)
  25     : d_context(c),
  26       d_ucontext(u),
  27       d_valuation(val),
  28       d_ee(nullptr),
  29       d_conflict(c, false)
  30 {
  31 }
  32
  33 void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
  34
  35 context::Context* TheoryState::getSatContext() const { return d_context; }
  36
  37 context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
  38
  39 bool TheoryState::hasTerm(TNode a) const
  40 {
  41   Assert(d_ee != nullptr);
  42   return d_ee->hasTerm(a);
  43 }
  44
  45 TNode TheoryState::getRepresentative(TNode t) const
  46 {
  47   Assert(d_ee != nullptr);
  48   if (d_ee->hasTerm(t))
  49   {
  50     return d_ee->getRepresentative(t);
  51   }
  52   return t;
  53 }
  54
  55 bool TheoryState::areEqual(TNode a, TNode b) const
  56 {
  57   Assert(d_ee != nullptr);
  58   if (a == b)
  59   {
  60     return true;
  61   }
  62   else if (hasTerm(a) && hasTerm(b))
  63   {
  64     return d_ee->areEqual(a, b);
  65   }
  66   return false;
  67 }
  68
  69 bool TheoryState::areDisequal(TNode a, TNode b) const
  70 {
  71   Assert(d_ee != nullptr);
  72   if (a == b)
  73   {
  74     return false;
  75   }
  76
  77   bool isConst = true;
  78   bool hasTerms = true;
  79   if (hasTerm(a))
  80   {
  81     a = d_ee->getRepresentative(a);
  82     isConst = a.isConst();
  83   }
  84   else if (!a.isConst())
  85   {
  86     // if not constant and not a term in the ee, it cannot be disequal
  87     return false;
  88   }
  89   else
  90   {
  91     hasTerms = false;
  92   }
  93
  94   if (hasTerm(b))
  95   {
  96     b = d_ee->getRepresentative(b);
  97     isConst = isConst && b.isConst();
  98   }
  99   else if (!b.isConst())
 100   {
 101     // same as above, it cannot be disequal
 102     return false;
 103   }
 104   else
 105   {
 106     hasTerms = false;
 107   }
 108
 109   if (isConst)
 110   {
 111     // distinct constants are disequal
 112     return a != b;
 113   }
 114   else if (!hasTerms)
 115   {
 116     return false;
 117   }
 118   // otherwise there may be an explicit disequality in the equality engine
 119   return d_ee->areDisequal(a, b, false);
 120 }
 121
 122 eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
 123
 124 void TheoryState::notifyInConflict() { d_conflict = true; }
 125
 126 bool TheoryState::isInConflict() const { return d_conflict; }
 127
 128 bool TheoryState::isSatLiteral(TNode lit) const
 129 {
 130   return d_valuation.isSatLiteral(lit);
 131 }
 132
 133 TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
 134
 135 bool TheoryState::hasSatValue(TNode n, bool& value) const
 136 {
 137   return d_valuation.hasSatValue(n, value);
 138 }
 139
 140 }  // namespace theory
 141 }  // namespace CVC4