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
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/ff/util.h"
      14                 :            : 
      15                 :            : // external includes
      16                 :            : #ifdef CVC5_USE_COCOA
      17                 :            : #include <CoCoA/QuotientRing.H>
      18                 :            : #endif /* CVC5_USE_COCOA */
      19                 :            : 
      20                 :            : // std includes
      21                 :            : #include <utility>
      22                 :            : 
      23                 :            : // internal includes
      24                 :            : #include "theory/theory.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace theory {
      28                 :            : namespace ff {
      29                 :            : 
      30                 :       2468 : FieldObj::FieldObj(NodeManager* nm, FfSize size)
      31                 :       2468 :     : d_size(std::move(size)),
      32                 :       2468 :       d_nm(nm),
      33                 :       2468 :       d_zero(d_nm->mkConst(FiniteFieldValue(0, d_size))),
      34                 :       2468 :       d_one(d_nm->mkConst(FiniteFieldValue(1, d_size)))
      35                 :            : {
      36                 :       2468 : }
      37                 :            : 
      38                 :            : template <bool ref_count>
      39                 :            : Node FieldObj::mkAdd(const std::vector<NodeTemplate<ref_count>>& summands)
      40                 :            : {
      41                 :            :   if (summands.empty())
      42                 :            :   {
      43                 :            :     return d_zero;
      44                 :            :   }
      45                 :            :   else if (summands.size() == 1)
      46                 :            :   {
      47                 :            :     return summands[0];
      48                 :            :   }
      49                 :            :   else
      50                 :            :   {
      51                 :            :     return d_nm->mkNode(Kind::FINITE_FIELD_ADD, std::move(summands));
      52                 :            :   }
      53                 :            : }
      54                 :            : 
      55                 :            : template <bool ref_count>
      56                 :            : Node FieldObj::mkMul(const std::vector<NodeTemplate<ref_count>>& factors)
      57                 :            : {
      58                 :            :   if (factors.empty())
      59                 :            :   {
      60                 :            :     return d_one;
      61                 :            :   }
      62                 :            :   else if (factors.size() == 1)
      63                 :            :   {
      64                 :            :     return factors[0];
      65                 :            :   }
      66                 :            :   else
      67                 :            :   {
      68                 :            :     return d_nm->mkNode(Kind::FINITE_FIELD_MULT, std::move(factors));
      69                 :            :   }
      70                 :            : }
      71                 :            : 
      72                 :      32581 : bool isFfLeaf(const Node& n)
      73                 :            : {
      74                 :      32581 :   return n.getType().isFiniteField() && Theory::isLeafOf(n, THEORY_FF);
      75                 :            : }
      76                 :            : 
      77                 :          0 : bool isFfTerm(const Node& n) { return n.getType().isFiniteField(); }
      78                 :            : 
      79                 :          0 : bool isFfFact(const Node& n)
      80                 :            : {
      81                 :          0 :   return (n.getKind() == Kind::EQUAL && n[0].getType().isFiniteField())
      82                 :          0 :          || (n.getKind() == Kind::NOT && n[0].getKind() == Kind::EQUAL
      83                 :          0 :              && n[0][0].getType().isFiniteField());
      84                 :            : }
      85                 :            : 
      86                 :          0 : FfTimeoutException::FfTimeoutException(const std::string& where)
      87                 :          0 :     : Exception(std::string("finite field solver timeout in ") + where)
      88                 :            : {
      89                 :          0 : }
      90                 :            : 
      91                 :          0 : FfTimeoutException::~FfTimeoutException() {}
      92                 :            : 
      93                 :     119819 : bool isFfLeaf(const Node& n, const FfSize& field)
      94                 :            : {
      95                 :     183544 :   return n.getType().isFiniteField() && Theory::isLeafOf(n, THEORY_FF)
      96 [ +  + ][ +  + ]:     303363 :          && n.getType().getFfSize() == field;
         [ +  + ][ +  + ]
                 [ -  - ]
      97                 :            : }
      98                 :            : 
      99                 :      31667 : bool isFfTerm(const Node& n, const FfSize& field)
     100                 :            : {
     101                 :      31667 :   return n.getType().isFiniteField() && n.getType().getFfSize() == field;
     102                 :            : }
     103                 :            : 
     104                 :     161641 : bool isFfFact(const Node& n, const FfSize& field)
     105                 :            : {
     106                 :     215023 :   return (n.getKind() == Kind::EQUAL && n[0].getType().isFiniteField()
     107                 :     215023 :           && n[0].getType().getFfSize() == field)
     108 [ +  + ][ +  + ]:     453256 :          || (n.getKind() == Kind::NOT && n[0].getKind() == Kind::EQUAL
         [ +  - ][ +  + ]
                 [ -  - ]
     109                 :     238233 :              && n[0][0].getType().isFiniteField()
     110                 :     399874 :              && n[0][0].getType().getFfSize() == field);
     111                 :            : }
     112                 :            : 
     113                 :            : }  // namespace ff
     114                 :            : }  // namespace theory
     115                 :            : }  // namespace cvc5::internal