Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner, Mudathir Mohamed
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * A theory state for Theory.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/theory_state.h"
      17                 :            : 
      18                 :            : #include "theory/uf/equality_engine.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : namespace theory {
      22                 :            : 
      23                 :     662943 : TheoryState::TheoryState(Env& env, Valuation val)
      24                 :            :     : EnvObj(env),
      25                 :            :       d_valuation(val),
      26                 :            :       d_ee(nullptr),
      27                 :          0 :       d_conflict(context(), false),
      28                 :     662943 :       d_sharedTerms(context())
      29                 :            : {
      30                 :     662943 : }
      31                 :            : 
      32                 :     662922 : void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
      33                 :            : 
      34                 :  737723000 : bool TheoryState::hasTerm(TNode t) const
      35                 :            : {
      36 [ -  + ][ -  + ]:  737723000 :   Assert(d_ee != nullptr);
                 [ -  - ]
      37                 :  737723000 :   return d_ee->hasTerm(t);
      38                 :            : }
      39                 :            : 
      40                 :          0 : void TheoryState::addTerm(TNode t)
      41                 :            : {
      42                 :          0 :   Assert(d_ee != nullptr);
      43                 :          0 :   d_ee->addTerm(t);
      44                 :          0 : }
      45                 :            : 
      46                 :  357964000 : TNode TheoryState::getRepresentative(TNode t) const
      47                 :            : {
      48 [ -  + ][ -  + ]:  357964000 :   Assert(d_ee != nullptr);
                 [ -  - ]
      49         [ +  + ]:  357964000 :   if (d_ee->hasTerm(t))
      50                 :            :   {
      51                 :  357634000 :     return d_ee->getRepresentative(t);
      52                 :            :   }
      53                 :     330166 :   return t;
      54                 :            : }
      55                 :            : 
      56                 :   19981200 : bool TheoryState::areEqual(TNode a, TNode b) const
      57                 :            : {
      58 [ -  + ][ -  + ]:   19981200 :   Assert(d_ee != nullptr);
                 [ -  - ]
      59         [ +  + ]:   19981200 :   if (a == b)
      60                 :            :   {
      61                 :    6080720 :     return true;
      62                 :            :   }
      63                 :   13900500 :   else if (hasTerm(a) && hasTerm(b))
      64                 :            :   {
      65                 :   13750900 :     return d_ee->areEqual(a, b);
      66                 :            :   }
      67                 :     149609 :   return false;
      68                 :            : }
      69                 :            : 
      70                 :    1922640 : bool TheoryState::areDisequal(TNode a, TNode b) const
      71                 :            : {
      72 [ -  + ][ -  + ]:    1922640 :   Assert(d_ee != nullptr);
                 [ -  - ]
      73         [ +  + ]:    1922640 :   if (a == b)
      74                 :            :   {
      75                 :     962977 :     return false;
      76                 :            :   }
      77                 :            : 
      78                 :     959666 :   bool isConst = true;
      79                 :     959666 :   bool hasTerms = true;
      80         [ +  + ]:     959666 :   if (hasTerm(a))
      81                 :            :   {
      82                 :     939699 :     a = d_ee->getRepresentative(a);
      83                 :     939699 :     isConst = a.isConst();
      84                 :            :   }
      85         [ +  + ]:      19967 :   else if (!a.isConst())
      86                 :            :   {
      87                 :            :     // if not constant and not a term in the ee, it cannot be disequal
      88                 :       4879 :     return false;
      89                 :            :   }
      90                 :            :   else
      91                 :            :   {
      92                 :      15088 :     hasTerms = false;
      93                 :            :   }
      94                 :            : 
      95         [ +  + ]:     954787 :   if (hasTerm(b))
      96                 :            :   {
      97                 :     939341 :     b = d_ee->getRepresentative(b);
      98 [ +  + ][ +  + ]:     939341 :     isConst = isConst && b.isConst();
      99                 :            :   }
     100         [ +  + ]:      15446 :   else if (!b.isConst())
     101                 :            :   {
     102                 :            :     // same as above, it cannot be disequal
     103                 :       1629 :     return false;
     104                 :            :   }
     105                 :            :   else
     106                 :            :   {
     107                 :      13817 :     hasTerms = false;
     108                 :            :   }
     109                 :            : 
     110         [ +  + ]:     953158 :   if (isConst)
     111                 :            :   {
     112                 :            :     // distinct constants are disequal
     113                 :     115615 :     return a != b;
     114                 :            :   }
     115         [ +  + ]:     837543 :   else if (!hasTerms)
     116                 :            :   {
     117                 :       2422 :     return false;
     118                 :            :   }
     119                 :            :   // otherwise there may be an explicit disequality in the equality engine
     120                 :     835121 :   return d_ee->areDisequal(a, b, false);
     121                 :            : }
     122                 :            : 
     123                 :          0 : void TheoryState::explainDisequal(TNode a, TNode b, std::vector<Node>& exp)
     124                 :            : {
     125                 :          0 :   if (hasTerm(a) && hasTerm(b) && d_ee->areDisequal(a, b, true))
     126                 :            :   {
     127                 :          0 :     exp.push_back(a.eqNode(b).notNode());
     128                 :          0 :     return;
     129                 :            :   }
     130                 :            :   // otherwise, add equalities to the (disequal) values
     131                 :          0 :   Node ar = getRepresentative(a);
     132         [ -  - ]:          0 :   if (ar != a)
     133                 :            :   {
     134                 :          0 :     exp.push_back(a.eqNode(ar));
     135                 :            :   }
     136                 :          0 :   Node br = getRepresentative(b);
     137         [ -  - ]:          0 :   if (br != b)
     138                 :            :   {
     139                 :          0 :     exp.push_back(b.eqNode(br));
     140                 :            :   }
     141                 :          0 :   Assert(ar != br && ar.isConst() && br.isConst());
     142                 :            : }
     143                 :            : 
     144                 :      15284 : void TheoryState::getEquivalenceClass(Node a, std::vector<Node>& eqc) const
     145                 :            : {
     146         [ +  + ]:      15284 :   if (d_ee->hasTerm(a))
     147                 :            :   {
     148                 :      30225 :     Node rep = d_ee->getRepresentative(a);
     149                 :      10075 :     eq::EqClassIterator eqc_iter(rep, d_ee);
     150         [ +  + ]:      71817 :     while (!eqc_iter.isFinished())
     151                 :            :     {
     152                 :      61742 :       eqc.push_back(*eqc_iter);
     153                 :      61742 :       eqc_iter++;
     154                 :            :     }
     155                 :            :   }
     156                 :            :   else
     157                 :            :   {
     158                 :       5209 :     eqc.push_back(a);
     159                 :            :   }
     160                 :            :   // a should be in its equivalence class
     161 [ -  + ][ -  + ]:      15284 :   Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end());
                 [ -  - ]
     162                 :      15284 : }
     163                 :            : 
     164                 :    1038470 : void TheoryState::addEqualityEngineTriggerPredicate(TNode pred)
     165                 :            : {
     166 [ -  + ][ -  + ]:    1038470 :   Assert(d_ee != nullptr);
                 [ -  - ]
     167 [ -  + ][ -  + ]:    1038470 :   Assert(pred.getType().isBoolean());
                 [ -  - ]
     168                 :            :   // if we don't already have a sat value
     169         [ +  + ]:    1038470 :   if (!d_valuation.hasSatValue(pred))
     170                 :            :   {
     171                 :            :     // Get triggered for both equal and dis-equal
     172                 :    1022370 :     d_ee->addTriggerPredicate(pred);
     173                 :            :   }
     174                 :            :   else
     175                 :            :   {
     176                 :            :     // otherwise we just add the term
     177                 :      16098 :     d_ee->addTerm(pred);
     178                 :            :   }
     179                 :    1038470 : }
     180                 :            : 
     181                 :   40655000 : eq::EqualityEngine* TheoryState::getEqualityEngine() const { return d_ee; }
     182                 :            : 
     183                 :    4639240 : void TheoryState::notifyInConflict() { d_conflict = true; }
     184                 :            : 
     185                 :  143267000 : bool TheoryState::isInConflict() const { return d_conflict; }
     186                 :            : 
     187                 :          0 : bool TheoryState::isSatLiteral(TNode lit) const
     188                 :            : {
     189                 :          0 :   return d_valuation.isSatLiteral(lit);
     190                 :            : }
     191                 :            : 
     192                 :     386023 : TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); }
     193                 :            : 
     194                 :       8228 : SortInference* TheoryState::getSortInference()
     195                 :            : {
     196                 :       8228 :   return d_valuation.getSortInference();
     197                 :            : }
     198                 :            : 
     199                 :      42897 : bool TheoryState::hasSatValue(TNode n, bool& value) const
     200                 :            : {
     201                 :      42897 :   return d_valuation.hasSatValue(n, value);
     202                 :            : }
     203                 :            : 
     204                 :     610325 : context::CDList<Assertion>::const_iterator TheoryState::factsBegin(TheoryId tid)
     205                 :            : {
     206                 :     610325 :   return d_valuation.factsBegin(tid);
     207                 :            : }
     208                 :     610325 : context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
     209                 :            : {
     210                 :     610325 :   return d_valuation.factsEnd(tid);
     211                 :            : }
     212                 :            : 
     213                 :    3719780 : Valuation& TheoryState::getValuation() { return d_valuation; }
     214                 :            : 
     215                 :    3708550 : void TheoryState::addSharedTerm(TNode node) { d_sharedTerms.push_back(node); }
     216                 :            : 
     217                 :            : }  // namespace theory
     218                 :            : }  // namespace cvc5::internal