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