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                 :            :  * CoCoA utilities
      11                 :            :  */
      12                 :            : 
      13                 :            : #ifdef CVC5_USE_COCOA
      14                 :            : 
      15                 :            : #include "theory/ff/cocoa_util.h"
      16                 :            : 
      17                 :            : // external includes
      18                 :            : #include <CoCoA/BigIntOps.H>
      19                 :            : #include <CoCoA/SparsePolyIter.H>
      20                 :            : #include <CoCoA/SparsePolyOps-RingElem.H>
      21                 :            : #include <CoCoA/SparsePolyOps-ideal.H>
      22                 :            : #include <CoCoA/TmpGPoly.H>
      23                 :            : 
      24                 :            : // std includes
      25                 :            : 
      26                 :            : // internal includes
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : namespace theory {
      30                 :            : namespace ff {
      31                 :            : 
      32                 :       1534 : std::optional<Scalar> cocoaEval(Poly poly, const PartialPoint& values)
      33                 :            : {
      34                 :       1534 :   CoCoA::ring coeffs = CoCoA::CoeffRing(CoCoA::owner(poly));
      35                 :       1534 :   Scalar out = CoCoA::zero(coeffs);
      36         [ +  + ]:       1912 :   for (auto it = CoCoA::BeginIter(poly), end = CoCoA::EndIter(poly); it != end;
      37                 :        378 :        ++it)
      38                 :            :   {
      39                 :       1769 :     Scalar term = CoCoA::coeff(it);
      40                 :       1769 :     std::vector<CoCoA::BigInt> exponents;
      41                 :       1769 :     CoCoA::BigExponents(exponents, CoCoA::PP(it));
      42         [ +  + ]:       6977 :     for (size_t i = 0, n = exponents.size(); i < n; ++i)
      43                 :            :     {
      44         [ +  + ]:       6599 :       if (!CoCoA::IsZero(exponents[i]))
      45                 :            :       {
      46         [ +  + ]:       1818 :         if (!values[i].has_value())
      47                 :            :         {
      48                 :       1391 :           return {};
      49                 :            :         }
      50                 :        427 :         term *= CoCoA::power(*values[i], exponents[i]);
      51                 :            :       }
      52                 :            :     }
      53                 :        378 :     out += term;
      54 [ +  + ][ +  + ]:       6085 :   }
         [ +  + ][ +  + ]
      55                 :        143 :   return {out};
      56                 :       1534 : }
      57                 :            : 
      58                 :       1201 : Scalar cocoaEval(Poly poly, const Point& values)
      59                 :            : {
      60                 :       1201 :   CoCoA::ring coeffs = CoCoA::CoeffRing(CoCoA::owner(poly));
      61                 :       1201 :   Scalar out = CoCoA::zero(coeffs);
      62         [ +  + ]:       3923 :   for (auto it = CoCoA::BeginIter(poly), end = CoCoA::EndIter(poly); it != end;
      63                 :       2722 :        ++it)
      64                 :            :   {
      65                 :       2722 :     Scalar term = CoCoA::coeff(it);
      66                 :       2722 :     std::vector<CoCoA::BigInt> exponents;
      67                 :       2722 :     CoCoA::BigExponents(exponents, CoCoA::PP(it));
      68         [ +  + ]:      19054 :     for (size_t i = 0, n = exponents.size(); i < n; ++i)
      69                 :            :     {
      70         [ +  + ]:      16332 :       if (!CoCoA::IsZero(exponents[i]))
      71                 :            :       {
      72                 :       3052 :         term *= CoCoA::power(values[i], exponents[i]);
      73                 :            :       }
      74                 :            :     }
      75                 :       2722 :     out += term;
      76                 :       3923 :   }
      77                 :       2402 :   return out;
      78                 :       1201 : }
      79                 :            : 
      80                 :       1313 : FiniteFieldValue cocoaFfToFfVal(const Scalar& elem, const FfSize& size)
      81                 :            : {
      82                 :       2626 :   return {Integer(extractStr(elem), 10), size};
      83                 :            : }
      84                 :            : 
      85                 :      10264 : CoCoA::BigInt intToCocoa(const Integer& i)
      86                 :            : {
      87                 :      20528 :   return CoCoA::BigIntFromString(i.toString());
      88                 :            : }
      89                 :            : 
      90                 :       7335 : const std::vector<Poly>& GBasisTimeout(const CoCoA::ideal& ideal,
      91                 :            :                                        const ResourceManager* rm)
      92                 :            : {
      93         [ +  + ]:       7335 :   if (rm == nullptr)
      94                 :            :   {
      95                 :        379 :     return CoCoA::GBasis(ideal);
      96                 :            :   }
      97                 :       6956 :   double sec = static_cast<double>(rm->getRemainingTime()) / 1e3;
      98         [ +  - ]:       6956 :   Trace("ff::gb") << "Computing a GB; limit " << sec << "s" << std::endl;
      99                 :            :   try
     100                 :            :   {
     101         [ +  + ]:       6956 :     if (sec == 0)
     102                 :            :     {
     103                 :       6951 :       return CoCoA::GBasis(ideal);
     104                 :            :     }
     105                 :            :     else
     106                 :            :     {
     107                 :          5 :       return CoCoA::GBasis(ideal, CoCoA::CpuTimeLimit(sec));
     108                 :            :     }
     109                 :            :   }
     110         [ -  - ]:          0 :   catch (CoCoA::TimeoutException& t)
     111                 :            :   {
     112                 :          0 :     CoCoA::handlersEnabled = false;
     113                 :          0 :     throw FfTimeoutException("GBasis");
     114                 :          0 :   }
     115                 :            : }
     116                 :            : 
     117                 :            : }  // namespace ff
     118                 :            : }  // namespace theory
     119                 :            : }  // namespace cvc5::internal
     120                 :            : 
     121                 :            : #endif /* CVC5_USE_COCOA */