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