Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Alex Ozdemir
       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                 :            :  * utilities
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "theory/ff/util.h"
      17                 :            : 
      18                 :            : // external includes
      19                 :            : #ifdef CVC5_USE_COCOA
      20                 :            : #include <CoCoA/QuotientRing.H>
      21                 :            : #endif /* CVC5_USE_COCOA */
      22                 :            : 
      23                 :            : // std includes
      24                 :            : 
      25                 :            : // internal includes
      26                 :            : #include "theory/ff/cocoa_util.h"
      27                 :            : #include "theory/theory.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace theory {
      31                 :            : namespace ff {
      32                 :            : 
      33                 :       3243 : FieldObj::FieldObj(const FfSize& size)
      34                 :            :     : d_size(size),
      35                 :       3243 :       d_nm(NodeManager::currentNM()),
      36                 :       6486 :       d_zero(d_nm->mkConst(FiniteFieldValue(0, d_size))),
      37                 :       6486 :       d_one(d_nm->mkConst(FiniteFieldValue(1, d_size)))
      38                 :            : #ifdef CVC5_USE_COCOA
      39                 :            :       ,
      40                 :      16215 :       d_coeffRing(CoCoA::NewZZmod(intToCocoa(d_size)))
      41                 :            : #endif /* CVC5_USE_COCOA */
      42                 :            : {
      43                 :       3243 : }
      44                 :            : 
      45                 :            : template <bool ref_count>
      46                 :            : Node FieldObj::mkAdd(const std::vector<NodeTemplate<ref_count>>& summands)
      47                 :            : {
      48                 :            :   if (summands.empty())
      49                 :            :   {
      50                 :            :     return d_zero;
      51                 :            :   }
      52                 :            :   else if (summands.size() == 1)
      53                 :            :   {
      54                 :            :     return summands[0];
      55                 :            :   }
      56                 :            :   else
      57                 :            :   {
      58                 :            :     return d_nm->mkNode(Kind::FINITE_FIELD_ADD, std::move(summands));
      59                 :            :   }
      60                 :            : }
      61                 :            : 
      62                 :            : template <bool ref_count>
      63                 :            : Node FieldObj::mkMul(const std::vector<NodeTemplate<ref_count>>& factors)
      64                 :            : {
      65                 :            :   if (factors.empty())
      66                 :            :   {
      67                 :            :     return d_one;
      68                 :            :   }
      69                 :            :   else if (factors.size() == 1)
      70                 :            :   {
      71                 :            :     return factors[0];
      72                 :            :   }
      73                 :            :   else
      74                 :            :   {
      75                 :            :     return d_nm->mkNode(Kind::FINITE_FIELD_MULT, std::move(factors));
      76                 :            :   }
      77                 :            : }
      78                 :            : 
      79                 :      35278 : bool isFfLeaf(const Node& n)
      80                 :            : {
      81                 :      35278 :   return n.getType().isFiniteField() && Theory::isLeafOf(n, THEORY_FF);
      82                 :            : }
      83                 :            : 
      84                 :          0 : bool isFfTerm(const Node& n) { return n.getType().isFiniteField(); }
      85                 :            : 
      86                 :          0 : bool isFfFact(const Node& n)
      87                 :            : {
      88                 :          0 :   return (n.getKind() == Kind::EQUAL && n[0].getType().isFiniteField())
      89                 :          0 :          || (n.getKind() == Kind::NOT && n[0].getKind() == Kind::EQUAL
      90                 :          0 :              && n[0][0].getType().isFiniteField());
      91                 :            : }
      92                 :            : 
      93                 :          0 : FfTimeoutException::FfTimeoutException(const std::string& where)
      94                 :          0 :     : Exception(std::string("finite field solver timeout in ") + where)
      95                 :            : {
      96                 :          0 : }
      97                 :            : 
      98                 :          0 : FfTimeoutException::~FfTimeoutException() {}
      99                 :            : 
     100                 :     194570 : bool isFfLeaf(const Node& n, const FfSize& field)
     101                 :            : {
     102                 :     288383 :   return n.getType().isFiniteField() && Theory::isLeafOf(n, THEORY_FF)
     103 [ +  + ][ +  + ]:     482953 :          && n.getType().getFfSize() == field;
         [ +  + ][ +  + ]
                 [ -  - ]
     104                 :            : }
     105                 :            : 
     106                 :      46710 : bool isFfTerm(const Node& n, const FfSize& field)
     107                 :            : {
     108                 :      46710 :   return n.getType().isFiniteField() && n.getType().getFfSize() == field;
     109                 :            : }
     110                 :            : 
     111                 :     275953 : bool isFfFact(const Node& n, const FfSize& field)
     112                 :            : {
     113                 :     359164 :   return (n.getKind() == Kind::EQUAL && n[0].getType().isFiniteField()
     114                 :     359164 :           && n[0].getType().getFfSize() == field)
     115 [ +  + ][ +  + ]:     781149 :          || (n.getKind() == Kind::NOT && n[0].getKind() == Kind::EQUAL
         [ +  - ][ +  + ]
                 [ -  - ]
     116                 :     421985 :              && n[0][0].getType().isFiniteField()
     117                 :     697938 :              && n[0][0].getType().getFfSize() == field);
     118                 :            : }
     119                 :            : 
     120                 :            : }  // namespace ff
     121                 :            : }  // namespace theory
     122                 :            : }  // namespace cvc5::internal