Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer
       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                 :            :  * Comparator utilities for the arithmetic rewriter.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__ARITH__REWRITER__ORDERING_H
      19                 :            : #define CVC5__THEORY__ARITH__REWRITER__ORDERING_H
      20                 :            : 
      21                 :            : #include "base/check.h"
      22                 :            : #include "expr/node.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal::theory::arith::rewriter {
      25                 :            : 
      26                 :            : /**
      27                 :            :  * Implements an ordering on arithmetic leaf nodes. We expect that values have
      28                 :            :  * already been combined, i.e., there shall only be a single rational and a
      29                 :            :  * single real algebraic number. It broadly categorizes leaf nodes into
      30                 :            :  * rationals, real algebraic numbers, integers, variables, and the rest.
      31                 :            :  * The ordering is built as follows:
      32                 :            :  * - rationals come first
      33                 :            :  * - real algebraic numbers come second
      34                 :            :  * - real terms come before integer terms
      35                 :            :  * - variables come before non-variable terms
      36                 :            :  * - finally, fall back to node ordering
      37                 :            :  */
      38                 :            : struct LeafNodeComparator
      39                 :            : {
      40                 :            :   /** Implements operator<(a, b) as described above */
      41                 :   58248300 :   bool operator()(TNode a, TNode b) const
      42                 :            :   {
      43         [ +  + ]:   58248300 :     if (a == b) return false;
      44                 :            : 
      45                 :   57884700 :     bool aIsConst = a.isConst();
      46                 :   57884700 :     bool bIsConst = b.isConst();
      47         [ +  + ]:   57884700 :     if (aIsConst != bIsConst) return aIsConst;
      48 [ +  - ][ +  - ]:   71842500 :     Assert(!aIsConst && !bIsConst) << "Rationals should be combined";
         [ -  + ][ -  - ]
      49                 :            : 
      50                 :   35921200 :     bool aIsRAN = a.getKind() == Kind::REAL_ALGEBRAIC_NUMBER;
      51                 :   35921200 :     bool bIsRAN = b.getKind() == Kind::REAL_ALGEBRAIC_NUMBER;
      52         [ +  + ]:   35921200 :     if (aIsRAN != bIsRAN) return aIsRAN;
      53 [ +  - ][ +  - ]:   71842500 :     Assert(!aIsRAN && !bIsRAN) << "real algebraic numbers should be combined";
         [ -  + ][ -  - ]
      54                 :            : 
      55                 :   35921200 :     bool aIsInt = a.getType().isInteger();
      56                 :   35921200 :     bool bIsInt = b.getType().isInteger();
      57         [ +  + ]:   35921200 :     if (aIsInt != bIsInt) return !aIsInt;
      58                 :            : 
      59                 :   35827000 :     bool aIsVar = a.isVar();
      60                 :   35827000 :     bool bIsVar = b.isVar();
      61         [ +  + ]:   35827000 :     if (aIsVar != bIsVar) return aIsVar;
      62                 :            : 
      63                 :   31491800 :     return a < b;
      64                 :            :   }
      65                 :            : };
      66                 :            : 
      67                 :            : /**
      68                 :            :  * Implements an ordering on arithmetic terms or summands. We expect these terms
      69                 :            :  * to be products (MULT or NONLINEAR_MULT), though products of zero or one node
      70                 :            :  * are not actually represented as such. For individual factors of the product,
      71                 :            :  * we rely on the ordering from LeafNodeComparator. Furthermore, we expect the
      72                 :            :  * individual factors to be sorted according to LeafNodeComparator. The ordering
      73                 :            :  * is built as follows:
      74                 :            :  * - single factors come first (everything that is MULT or NONLINEAR_MULT)
      75                 :            :  * - multiplications with less factors come first
      76                 :            :  * - multiplications are compared lexicographically
      77                 :            :  */
      78                 :            : struct TermComparator
      79                 :            : {
      80                 :            :   /** Implements operator<(a, b) as described above */
      81                 :   63649100 :   bool operator()(TNode a, TNode b) const
      82                 :            :   {
      83         [ +  + ]:   63649100 :     if (a == b) return false;
      84                 :            : 
      85                 :            :     bool aIsMult =
      86 [ +  - ][ +  + ]:   59917400 :         a.getKind() == Kind::MULT || a.getKind() == Kind::NONLINEAR_MULT;
      87                 :            :     bool bIsMult =
      88 [ +  - ][ +  + ]:   59917400 :         b.getKind() == Kind::MULT || b.getKind() == Kind::NONLINEAR_MULT;
      89         [ +  + ]:   59917400 :     if (aIsMult != bIsMult) return !aIsMult;
      90                 :            : 
      91         [ +  + ]:   57634400 :     if (!aIsMult)
      92                 :            :     {
      93                 :   53063600 :       return LeafNodeComparator()(a, b);
      94                 :            :     }
      95                 :            : 
      96                 :    4570800 :     size_t aLen = a.getNumChildren();
      97                 :    4570800 :     size_t bLen = b.getNumChildren();
      98         [ +  + ]:    4570800 :     if (aLen != bLen) return aLen < bLen;
      99                 :            : 
     100         [ +  - ]:    6830910 :     for (size_t i = 0; i < aLen; ++i)
     101                 :            :     {
     102         [ +  + ]:    6830910 :       if (a[i] != b[i])
     103                 :            :       {
     104                 :    4303560 :         return LeafNodeComparator()(a[i], b[i]);
     105                 :            :       }
     106                 :            :     }
     107                 :          0 :     Unreachable() << "Nodes are different, but have the same content";
     108                 :            :     return false;
     109                 :            :   }
     110                 :            : };
     111                 :            : 
     112                 :            : }  // namespace cvc5::internal::theory::arith::rewriter
     113                 :            : 
     114                 :            : #endif