Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A theory state for Theory.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/theory_state.h"
      14                 :            : 
      15                 :            : #include "theory/uf/equality_engine.h"
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : namespace theory {
      19                 :            : 
      20                 :     664269 : TheoryState::TheoryState(Env& env, Valuation val)
      21                 :            :     : EnvObj(env),
      22                 :     664269 :       d_valuation(val),
      23                 :     664269 :       d_ee(nullptr),
      24                 :     664269 :       d_conflict(context(), false),
      25                 :    1328538 :       d_sharedTerms(context())
      26                 :            : {
      27                 :     664269 : }
      28                 :            : 
      29                 :     664248 : void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
      30                 :            : 
      31                 :  106399176 : bool TheoryState::hasTerm(TNode t) const
      32                 :            : {
      33 [ -  + ][ -  + ]:  106399176 :   Assert(d_ee != nullptr);
                 [ -  - ]
      34                 :  106399176 :   return d_ee->hasTerm(t);
      35                 :            : }
      36                 :            : 
      37                 :     148138 : void TheoryState::addTerm(TNode t)
      38                 :            : {
      39 [ -  + ][ -  + ]:     148138 :   Assert(d_ee != nullptr);
                 [ -  - ]
      40                 :     148138 :   d_ee->addTerm(t);
      41                 :     148138 : }
      42                 :            : 
      43                 :   61430971 : TNode TheoryState::getRepresentative(TNode t) const
      44                 :            : {
      45 [ -  + ][ -  + ]:   61430971 :   Assert(d_ee != nullptr);
                 [ -  - ]
      46         [ +  + ]:   61430971 :   if (d_ee->hasTerm(t))
      47                 :            :   {
      48                 :   61128086 :     return d_ee->getRepresentative(t);
      49                 :            :   }
      50                 :     302885 :   return t;
      51                 :            : }
      52                 :            : 
      53                 :   24506465 : bool TheoryState::areEqual(TNode a, TNode b) const
      54                 :            : {
      55 [ -  + ][ -  + ]:   24506465 :   Assert(d_ee != nullptr);
                 [ -  - ]
      56         [ +  + ]:   24506465 :   if (a == b)
      57                 :            :   {
      58                 :    8418354 :     return true;
      59                 :            :   }
      60                 :   16088111 :   else if (hasTerm(a) && hasTerm(b))
      61                 :            :   {
      62                 :   15910143 :     return d_ee->areEqual(a, b);
      63                 :            :   }
      64                 :     177968 :   return false;
      65                 :            : }
      66                 :            : 
      67                 :    3167181 : bool TheoryState::areDisequal(TNode a, TNode b) const
      68                 :            : {
      69 [ -  + ][ -  + ]:    3167181 :   Assert(d_ee != nullptr);
                 [ -  - ]
      70         [ +  + ]:    3167181 :   if (a == b)
      71                 :            :   {
      72                 :    1008612 :     return false;
      73                 :            :   }
      74                 :            : 
      75                 :    2158569 :   bool isConst = true;
      76                 :    2158569 :   bool hasTerms = true;
      77         [ +  + ]:    2158569 :   if (hasTerm(a))
      78                 :            :   {
      79                 :    2090017 :     a = d_ee->getRepresentative(a);
      80                 :    2090017 :     isConst = a.isConst();
      81                 :            :   }
      82         [ +  + ]:      68552 :   else if (!a.isConst())
      83                 :            :   {
      84                 :            :     // if not constant and not a term in the ee, it cannot be disequal
      85                 :      48521 :     return false;
      86                 :            :   }
      87                 :            :   else
      88                 :            :   {
      89                 :      20031 :     hasTerms = false;
      90                 :            :   }
      91                 :            : 
      92         [ +  + ]:    2110048 :   if (hasTerm(b))
      93                 :            :   {
      94                 :    2096342 :     b = d_ee->getRepresentative(b);
      95 [ +  + ][ +  + ]:    2096342 :     isConst = isConst && b.isConst();
      96                 :            :   }
      97         [ +  + ]:      13706 :   else if (!b.isConst())
      98                 :            :   {
      99                 :            :     // same as above, it cannot be disequal
     100                 :       1348 :     return false;
     101                 :            :   }
     102                 :            :   else
     103                 :            :   {
     104                 :      12358 :     hasTerms = false;
     105                 :            :   }
     106                 :            : 
     107         [ +  + ]:    2108700 :   if (isConst)
     108                 :            :   {
     109                 :            :     // distinct constants are disequal
     110                 :     280447 :     return a != b;
     111                 :            :   }
     112         [ +  + ]:    1828253 :   else if (!hasTerms)
     113                 :            :   {
     114                 :       2734 :     return false;
     115                 :            :   }
     116                 :            :   // otherwise there may be an explicit disequality in the equality engine
     117                 :    1825519 :   return d_ee->areDisequal(a, b, false);
     118                 :            : }
     119                 :            : 
     120                 :          0 : void TheoryState::explainDisequal(TNode a, TNode b, std::vector<Node>& exp)
     121                 :            : {
     122                 :          0 :   if (hasTerm(a) && hasTerm(b) && d_ee->areDisequal(a, b, true))
     123                 :            :   {
     124                 :          0 :     exp.push_back(a.eqNode(b).notNode());
     125                 :          0 :     return;
     126                 :            :   }
     127                 :            :   // otherwise, add equalities to the (disequal) values
     128                 :          0 :   Node ar = getRepresentative(a);
     129         [ -  - ]:          0 :   if (ar != a)
     130                 :            :   {
     131                 :          0 :     exp.push_back(a.eqNode(ar));
     132                 :            :   }
     133                 :          0 :   Node br = getRepresentative(b);
     134         [ -  - ]:          0 :   if (br != b)
     135                 :            :   {
     136                 :          0 :     exp.push_back(b.eqNode(br));
     137                 :            :   }
     138                 :          0 :   Assert(ar != br && ar.isConst() && br.isConst());
     139                 :          0 : }
     140                 :            : 
     141                 :      16224 : void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
     142                 :            : {
     143         [ +  + ]:      16224 :   if (d_ee->hasTerm(a))
     144                 :            :   {
     145                 :      20914 :     Node rep = d_ee->getRepresentative(a);
     146                 :      10457 :     eq::EqClassIterator eqc_iter(rep, d_ee);
     147         [ +  + ]:      74902 :     while (!eqc_iter.isFinished())
     148                 :            :     {
     149                 :      64445 :       eqc.push_back(*eqc_iter);
     150                 :      64445 :       eqc_iter++;
     151                 :            :     }
     152                 :      10457 :   }
     153                 :            :   else
     154                 :            :   {
     155                 :       5767 :     eqc.push_back(a);
     156                 :            :   }
     157                 :            :   // a should be in its equivalence class
     158 [ -  + ][ -  + ]:      16224 :   Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
                 [ -  - ]
     159                 :      16224 : }
     160                 :            : 
     161                 :     935965 : void TheoryState::addEqualityEngineTriggerPredicate(TNode pred)
     162                 :            : {
     163 [ -  + ][ -  + ]:     935965 :   Assert(d_ee != nullptr);
                 [ -  - ]
     164 [ -  + ][ -  + ]:     935965 :   Assert(pred.getType().isBoolean());
                 [ -  - ]
     165                 :            :   // if we don't already have a sat value
     166         [ +  + ]:     935965 :   if (!d_valuation.hasSatValue(pred))
     167                 :            :   {
     168                 :            :     // Get triggered for both equal and dis-equal
     169                 :     920954 :     d_ee->addTriggerPredicate(pred);
     170                 :            :   }
     171                 :            :   else
     172                 :            :   {
     173                 :            :     // otherwise we just add the term
     174                 :      15011 :     d_ee->addTerm(pred);
     175                 :            :   }
     176                 :     935965 : }
     177                 :            : 
     178                 :   51907571 : eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
     179                 :            : 
     180                 :    5198879 : void TheoryState::notifyInConflict() { d_conflict = true; }
     181                 :            : 
     182                 :  118375624 : bool TheoryState::isInConflict() const { return d_conflict; }
     183                 :            : 
     184                 :          0 : bool TheoryState::isSatLiteral(TNode lit) const
     185                 :            : {
     186                 :          0 :   return d_valuation.isSatLiteral(lit);
     187                 :            : }
     188                 :            : 
     189                 :     389677 : TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
     190                 :            : 
     191                 :       8118 : SortInference* TheoryState::getSortInference()
     192                 :            : {
     193                 :       8118 :   return d_valuation.getSortInference();
     194                 :            : }
     195                 :            : 
     196                 :      49700 : bool TheoryState::hasSatValue(TNode n, bool& value) const
     197                 :            : {
     198                 :      49700 :   return d_valuation.hasSatValue(n, value);
     199                 :            : }
     200                 :            : 
     201                 :     655998 : context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
     202                 :            : {
     203                 :     655998 :   return d_valuation.factsBegin(tid);
     204                 :            : }
     205                 :     655998 : context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
     206                 :            : {
     207                 :     655998 :   return d_valuation.factsEnd(tid);
     208                 :            : }
     209                 :            : 
     210                 :    4817972 : Valuation& TheoryState::getValuation() { return d_valuation; }
     211                 :            : 
     212                 :    3725188 : void TheoryState::addSharedTerm(TNode node) { d_sharedTerms.push_back(node); }
     213                 :            : 
     214                 :            : }  // namespace theory
     215                 :            : }  // namespace cvc5::internal