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                 :            :  */
      11                 :            : 
      12                 :            : #ifdef CVC5_USE_COCOA
      13                 :            : 
      14                 :            : #include "theory/ff/gb.h"
      15                 :            : 
      16                 :            : // external includes
      17                 :            : #include <CoCoA/ideal.H>
      18                 :            : #include <CoCoA/ring.H>
      19                 :            : #include <CoCoA/symbol.H>
      20                 :            : 
      21                 :            : // internal includes
      22                 :            : #include "options/ff_options.h"
      23                 :            : #include "theory/ff/cocoa_encoder.h"
      24                 :            : #include "theory/ff/multi_roots.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace theory {
      28                 :            : namespace ff {
      29                 :            : 
      30                 :       1807 : FfResult gb(const std::vector<Node>& facts,
      31                 :            :             const FfSize& size,
      32                 :            :             const Env& env,
      33                 :            :             FfStatistics* stats)
      34                 :            : {
      35                 :       1807 :   CocoaEncoder enc(env.getNodeManager(), size);
      36                 :            :   // collect leaves
      37         [ +  + ]:      46681 :   for (const Node& node : facts)
      38                 :            :   {
      39                 :      44874 :     enc.addFact(node);
      40                 :            :   }
      41                 :       1807 :   enc.endScan();
      42                 :            :   // assert facts
      43         [ +  + ]:      46681 :   for (const Node& node : facts)
      44                 :            :   {
      45                 :      44874 :     enc.addFact(node);
      46                 :            :   }
      47                 :            : 
      48                 :            :   // compute a GB
      49                 :       1807 :   std::vector<CoCoA::RingElem> generators;
      50                 :       1807 :   generators.insert(generators.end(), enc.polys().begin(), enc.polys().end());
      51                 :       5421 :   generators.insert(
      52                 :       5421 :       generators.end(), enc.bitsumPolys().begin(), enc.bitsumPolys().end());
      53         [ +  + ]:       1807 :   if (env.getOptions().ff.ffFieldPolys)
      54                 :            :   {
      55                 :         11 :     CoCoA::PolyRing polyRing(enc.polyRing());
      56         [ +  + ]:         24 :     for (const auto& var : CoCoA::indets(polyRing))
      57                 :            :     {
      58                 :         13 :       CoCoA::BigInt characteristic = CoCoA::characteristic(enc.coeffRing());
      59                 :         13 :       const long power = CoCoA::LogCardinality(enc.coeffRing());
      60                 :         13 :       CoCoA::BigInt s = CoCoA::power(characteristic, power);
      61                 :         13 :       generators.push_back(CoCoA::power(var, s) - var);
      62                 :         13 :     }
      63                 :         11 :   }
      64                 :       1807 :   Tracer tracer(generators);
      65         [ +  - ]:       1807 :   if (stats) ++stats->d_numGbRuns;
      66         [ +  - ]:       1807 :   if (env.getOptions().ff.ffTraceGb) tracer.setFunctionPointers();
      67                 :       1807 :   const CoCoA::ideal ideal = CoCoA::ideal(generators);
      68                 :       1807 :   std::vector<Poly> basis;
      69                 :            :   {
      70         [ +  - ]:       1807 :     CodeTimer timer(stats ? &stats->d_timeGbRuns : nullptr);
      71                 :       1807 :     basis = GBasisTimeout(ideal, env.getResourceManager());
      72                 :       1807 :   }
      73         [ +  - ]:       1807 :   if (env.getOptions().ff.ffTraceGb) tracer.unsetFunctionPointers();
      74                 :            : 
      75                 :            :   // if it is trivial, create a conflict
      76 [ +  + ][ +  + ]:       1807 :   bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
      77         [ +  + ]:       1807 :   if (is_trivial)
      78                 :            :   {
      79         [ +  - ]:       1695 :     Trace("ff::gb") << "Trivial GB" << std::endl;
      80         [ +  - ]:       1695 :     if (stats) ++stats->d_numTrivialUnsat;
      81         [ +  - ]:       1695 :     if (env.getOptions().ff.ffTraceGb)
      82                 :            :     {
      83                 :       1695 :       std::vector<size_t> coreIndices = tracer.trace(basis.front());
      84                 :       1695 :       FfCore conflict;
      85         [ +  + ]:      46162 :       for (size_t i = 0, n = facts.size(); i < n; ++i)
      86                 :            :       {
      87         [ +  - ]:      44467 :         Trace("ff::core") << "In " << i << " : " << facts[i] << std::endl;
      88                 :            :       }
      89         [ +  + ]:      13610 :       for (size_t i : coreIndices)
      90                 :            :       {
      91                 :            :         // omit (field polys, bitsum polys, ...) from core
      92         [ +  + ]:      11915 :         if (enc.polyHasFact(generators[i]))
      93                 :            :         {
      94         [ +  - ]:      11903 :           Trace("ff::core") << "Core: " << i << " : " << facts[i] << std::endl;
      95                 :      11903 :           conflict.push_back(enc.polyFact(generators[i]));
      96                 :            :         }
      97                 :            :       }
      98                 :       1695 :       return conflict;
      99                 :       1695 :     }
     100                 :            :     else
     101                 :            :     {
     102                 :            :       // set trivial conflict
     103                 :          0 :       return facts;
     104                 :            :     }
     105                 :            :   }
     106                 :            :   else
     107                 :            :   {
     108         [ +  - ]:        112 :     Trace("ff::gb") << "Non-trivial GB" << std::endl;
     109                 :            : 
     110                 :            :     // common root (vec of CoCoA base ring elements)
     111                 :            : 
     112                 :        112 :     std::vector<CoCoA::RingElem> root;
     113                 :            :     {
     114         [ +  - ]:        112 :       CodeTimer timer(stats ? &stats->d_modelConstructionTime : nullptr);
     115                 :        112 :       root = findZero(ideal, env, stats);
     116                 :        112 :     }
     117                 :            : 
     118         [ +  + ]:        112 :     if (root.empty())
     119                 :            :     {
     120                 :            :       // set trivial conflict
     121                 :          9 :       return facts;
     122                 :            :     }
     123                 :            :     else
     124                 :            :     {
     125                 :        103 :       FfModel model;
     126         [ +  + ]:        390 :       for (const auto& [idx, node] : enc.nodeIndets())
     127                 :            :       {
     128         [ +  - ]:        287 :         if (isFfLeaf(node))
     129                 :            :         {
     130                 :        287 :           model.emplace(node, enc.cocoaFfToFfVal(root[idx]));
     131                 :            :         }
     132                 :        103 :       }
     133                 :        103 :       return model;
     134                 :        103 :     }
     135                 :        112 :   }
     136                 :       1807 : }
     137                 :            : 
     138                 :            : }  // namespace ff
     139                 :            : }  // namespace theory
     140                 :            : }  // namespace cvc5::internal
     141                 :            : 
     142                 :            : #endif