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                 :            :  * Utilities for cardinality classes.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "util/cardinality_class.h"
      14                 :            : 
      15                 :            : #include <iostream>
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : 
      19                 :          0 : const char* toString(CardinalityClass c)
      20                 :            : {
      21 [ -  - ][ -  - ]:          0 :   switch (c)
            [ -  - ][ - ]
      22                 :            :   {
      23                 :          0 :     case CardinalityClass::ONE: return "ONE";
      24                 :          0 :     case CardinalityClass::INTERPRETED_ONE: return "INTERPRETED_ONE";
      25                 :          0 :     case CardinalityClass::FINITE: return "FINITE";
      26                 :          0 :     case CardinalityClass::INTERPRETED_FINITE: return "INTERPRETED_FINITE";
      27                 :          0 :     case CardinalityClass::INFINITE: return "INFINITE";
      28                 :          0 :     case CardinalityClass::UNKNOWN: return "UNKNOWN";
      29                 :          0 :     default: return "?CardinalityClass?";
      30                 :            :   }
      31                 :            : }
      32                 :            : 
      33                 :          0 : std::ostream& operator<<(std::ostream& out, CardinalityClass c)
      34                 :            : {
      35                 :          0 :   out << toString(c);
      36                 :          0 :   return out;
      37                 :            : }
      38                 :            : 
      39                 :      53135 : CardinalityClass maxCardinalityClass(CardinalityClass c1, CardinalityClass c2)
      40                 :            : {
      41                 :            :   // If one of the classes is interpreted one and the other finite, then the
      42                 :            :   // result should be interpreted finite: the type is finite under the
      43                 :            :   // assumption that uninterpreted sorts have cardinality one, but infinite
      44                 :            :   // otherwise.
      45         [ +  + ]:      53135 :   if ((c1 == CardinalityClass::INTERPRETED_ONE
      46         [ +  + ]:        367 :        && c2 == CardinalityClass::FINITE)
      47         [ +  + ]:      53134 :       || (c1 == CardinalityClass::FINITE
      48         [ +  + ]:      15164 :           && c2 == CardinalityClass::INTERPRETED_ONE))
      49                 :            :   {
      50                 :        531 :     return CardinalityClass::INTERPRETED_FINITE;
      51                 :            :   }
      52         [ +  + ]:      52604 :   return c1 > c2 ? c1 : c2;
      53                 :            : }
      54                 :            : 
      55                 :   18034972 : bool isCardinalityClassFinite(CardinalityClass c, bool fmfEnabled)
      56                 :            : {
      57 [ +  + ][ +  + ]:   18034972 :   if (c == CardinalityClass::ONE || c == CardinalityClass::FINITE)
      58                 :            :   {
      59                 :    1628246 :     return true;
      60                 :            :   }
      61         [ +  + ]:   16406726 :   if (fmfEnabled)
      62                 :            :   {
      63                 :            :     // if finite model finding is enabled, interpreted one/finite are also
      64                 :            :     // considered finite.
      65                 :            :     return c == CardinalityClass::INTERPRETED_ONE
      66 [ +  + ][ +  + ]:     301885 :            || c == CardinalityClass::INTERPRETED_FINITE;
      67                 :            :   }
      68                 :   16104841 :   return false;
      69                 :            : }
      70                 :            : 
      71                 :            : }  // namespace cvc5::internal