Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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                 :            :  * Implementation of term context utilities.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "expr/term_context.h"
      17                 :            : 
      18                 :            : #include "theory/theory.h"
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : 
      22                 :          0 : uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const
      23                 :            : {
      24                 :            :   // default is no change
      25                 :          0 :   return tval;
      26                 :            : }
      27                 :            : 
      28                 :    1749510 : uint32_t RtfTermContext::initialValue() const
      29                 :            : {
      30                 :            :   // by default, not in a term context or a quantifier
      31                 :    1749510 :   return 0;
      32                 :            : }
      33                 :            : 
      34                 :   24312800 : uint32_t RtfTermContext::computeValue(TNode t,
      35                 :            :                                       uint32_t tval,
      36                 :            :                                       size_t child) const
      37                 :            : {
      38         [ +  + ]:   24312800 :   if (t.isClosure())
      39                 :            :   {
      40         [ +  + ]:       5136 :     if (tval % 2 == 0)
      41                 :            :     {
      42                 :       4744 :       return tval + 1;
      43                 :            :     }
      44                 :            :   }
      45         [ +  + ]:   24307700 :   else if (hasNestedTermChildren(t))
      46                 :            :   {
      47         [ +  + ]:    5503860 :     if (tval < 2)
      48                 :            :     {
      49                 :    3063320 :       return tval + 2;
      50                 :            :     }
      51                 :            :   }
      52                 :   21244700 :   return tval;
      53                 :            : }
      54                 :            : 
      55                 :          0 : uint32_t RtfTermContext::getValue(bool inQuant, bool inTerm)
      56                 :            : {
      57 [ -  - ][ -  - ]:          0 :   return (inQuant ? 1 : 0) + 2 * (inTerm ? 1 : 0);
      58                 :            : }
      59                 :            : 
      60                 :    4987530 : void RtfTermContext::getFlags(uint32_t val, bool& inQuant, bool& inTerm)
      61                 :            : {
      62                 :    4987530 :   inQuant = val % 2 == 1;
      63                 :    4987530 :   inTerm = val >= 2;
      64                 :    4987530 : }
      65                 :            : 
      66                 :   24307700 : bool RtfTermContext::hasNestedTermChildren(TNode t)
      67                 :            : {
      68                 :   24307700 :   Kind k = t.getKind();
      69                 :            :   // dont' worry about FORALL or EXISTS, these are part of inQuant.
      70         [ +  + ]:   32781800 :   return theory::kindToTheoryId(k) != theory::THEORY_BOOL && k != Kind::EQUAL
      71 [ +  + ][ +  + ]:    5512820 :          && k != Kind::SEP_STAR && k != Kind::SEP_WAND && k != Kind::SEP_LABEL
                 [ +  + ]
      72 [ +  + ][ +  + ]:   32781800 :          && k != Kind::BITVECTOR_EAGER_ATOM;
      73                 :            : }
      74                 :            : 
      75                 :          0 : uint32_t InQuantTermContext::initialValue() const { return 0; }
      76                 :            : 
      77                 :          0 : uint32_t InQuantTermContext::computeValue(TNode t,
      78                 :            :                                           uint32_t tval,
      79                 :            :                                           size_t index) const
      80                 :            : {
      81         [ -  - ]:          0 :   return t.isClosure() ? 1 : tval;
      82                 :            : }
      83                 :            : 
      84         [ -  - ]:          0 : uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
      85                 :            : 
      86                 :          0 : bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
      87                 :            : {
      88                 :          0 :   return val == 1;
      89                 :            : }
      90                 :            : 
      91                 :      15032 : uint32_t PolarityTermContext::initialValue() const
      92                 :            : {
      93                 :            :   // by default, we have true polarity
      94                 :      15032 :   return 2;
      95                 :            : }
      96                 :            : 
      97                 :     197902 : uint32_t PolarityTermContext::computeValue(TNode t,
      98                 :            :                                            uint32_t tval,
      99                 :            :                                            size_t index) const
     100                 :            : {
     101 [ +  + ][ +  + ]:     197902 :   switch (t.getKind())
                 [ -  + ]
     102                 :            :   {
     103                 :      19208 :     case Kind::AND:
     104                 :            :     case Kind::OR:
     105                 :            :     case Kind::SEP_STAR:
     106                 :            :       // polarity preserved
     107                 :      19208 :       return tval;
     108                 :         72 :     case Kind::IMPLIES:
     109                 :            :       // first child reverses, otherwise we preserve
     110 [ +  + ][ +  - ]:         72 :       return index == 0 ? (tval == 0 ? 0 : (3 - tval)) : tval;
     111                 :      17685 :     case Kind::NOT:
     112                 :            :       // polarity reversed
     113         [ +  + ]:      17685 :       return tval == 0 ? 0 : (3 - tval);
     114                 :       1867 :     case Kind::ITE:
     115                 :            :       // head has no polarity, branches preserve
     116         [ +  + ]:       1867 :       return index == 0 ? 0 : tval;
     117                 :          0 :     case Kind::FORALL:
     118                 :            :       // body preserves, others have no polarity.
     119         [ -  - ]:          0 :       return index == 1 ? tval : 0;
     120                 :     159070 :     default:
     121                 :            :       // no polarity
     122                 :     159070 :       break;
     123                 :            :   }
     124                 :     159070 :   return 0;
     125                 :            : }
     126                 :            : 
     127                 :          0 : uint32_t PolarityTermContext::getValue(bool hasPol, bool pol)
     128                 :            : {
     129 [ -  - ][ -  - ]:          0 :   return hasPol ? (pol ? 2 : 1) : 0;
     130                 :            : }
     131                 :            : 
     132                 :      65685 : void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol)
     133                 :            : {
     134                 :      65685 :   hasPol = val != 0;
     135                 :      65685 :   pol = val == 2;
     136                 :      65685 : }
     137                 :            : 
     138                 :      12680 : uint32_t TheoryLeafTermContext::initialValue() const { return 0; }
     139                 :            : 
     140                 :      86308 : uint32_t TheoryLeafTermContext::computeValue(TNode t,
     141                 :            :                                              uint32_t tval,
     142                 :            :                                              size_t index) const
     143                 :            : {
     144         [ +  + ]:      86308 :   return theory::Theory::isLeafOf(t, d_theoryId) ? 1 : tval;
     145                 :            : }
     146                 :            : 
     147                 :            : }  // namespace cvc5::internal