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                 :            :  * Finite fields theory.
      11                 :            :  *
      12                 :            :  * There is a subtheory for each prime p that handles the field Fp. Essentially
      13                 :            :  * the common theory just multiplexes the sub-theories.
      14                 :            :  *
      15                 :            :  * NB: while most of FF does not build without CoCoA, this class does. So, it
      16                 :            :  * has many ifdef blocks that throw errors without CoCoA.
      17                 :            :  */
      18                 :            : 
      19                 :            : #include "theory/ff/theory_ff.h"
      20                 :            : 
      21                 :            : #include <cerrno>
      22                 :            : #include <fstream>
      23                 :            : #include <iostream>
      24                 :            : #include <numeric>
      25                 :            : #include <sstream>
      26                 :            : #include <unordered_map>
      27                 :            : 
      28                 :            : #include "expr/node_traversal.h"
      29                 :            : #include "options/ff_options.h"
      30                 :            : #include "theory/ff/util.h"
      31                 :            : #include "theory/theory_model.h"
      32                 :            : #include "theory/trust_substitutions.h"
      33                 :            : #include "util/result.h"
      34                 :            : #include "util/statistics_registry.h"
      35                 :            : #include "util/utility.h"
      36                 :            : 
      37                 :            : using namespace cvc5::internal::kind;
      38                 :            : 
      39                 :            : namespace cvc5::internal {
      40                 :            : namespace theory {
      41                 :            : namespace ff {
      42                 :            : 
      43                 :          0 : void noCoCoA()
      44                 :            : {
      45                 :          0 :   throw LogicException(
      46                 :            :       "cvc5 can't solve field problems since it was not configured with "
      47                 :          0 :       "--cocoa");
      48                 :            : }
      49                 :            : 
      50                 :      51003 : TheoryFiniteFields::TheoryFiniteFields(Env& env,
      51                 :            :                                        OutputChannel& out,
      52                 :      51003 :                                        Valuation valuation)
      53                 :            :     : Theory(THEORY_FF, env, out, valuation),
      54                 :      51003 :       d_rewriter(nodeManager()),
      55                 :      51003 :       d_state(env, valuation),
      56                 :      51003 :       d_im(env, *this, d_state, getStatsPrefix(THEORY_FF)),
      57                 :      51003 :       d_eqNotify(d_im),
      58                 :      51003 :       d_stats(
      59                 :     102006 :           std::make_unique<FfStatistics>(statisticsRegistry(), "theory::ff::"))
      60                 :            : {
      61                 :      51003 :   d_theoryState = &d_state;
      62                 :      51003 :   d_inferManager = &d_im;
      63                 :      51003 : }
      64                 :            : 
      65                 :     101316 : TheoryFiniteFields::~TheoryFiniteFields() {}
      66                 :            : 
      67                 :      51003 : TheoryRewriter* TheoryFiniteFields::getTheoryRewriter()
      68                 :            : {
      69         [ +  + ]:      51003 :   if (!options().ff.ff)
      70                 :            :   {
      71                 :          5 :     return nullptr;
      72                 :            :   }
      73                 :      50998 :   return &d_rewriter;
      74                 :            : }
      75                 :            : 
      76                 :      19827 : ProofRuleChecker* TheoryFiniteFields::getProofChecker() { return nullptr; }
      77                 :            : 
      78                 :      51003 : bool TheoryFiniteFields::needsEqualityEngine(EeSetupInfo& esi)
      79                 :            : {
      80                 :      51003 :   esi.d_notify = &d_eqNotify;
      81                 :      51003 :   esi.d_name = "theory::ff::ee";
      82                 :      51003 :   return true;
      83                 :            : }
      84                 :            : 
      85                 :      51003 : void TheoryFiniteFields::finishInit()
      86                 :            : {
      87 [ -  + ][ -  + ]:      51003 :   Assert(d_equalityEngine != nullptr);
                 [ -  - ]
      88                 :            : 
      89                 :      51003 :   d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_MULT);
      90                 :      51003 :   d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_NEG);
      91                 :      51003 :   d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_ADD);
      92                 :      51003 : }
      93                 :            : 
      94                 :      83341 : void TheoryFiniteFields::postCheck(CVC5_UNUSED Effort level)
      95                 :            : {
      96                 :            : #ifdef CVC5_USE_COCOA
      97         [ +  - ]:     166682 :   Trace("ff::check") << "ff::check : " << level << " @ level "
      98                 :      83341 :                      << context()->getLevel() << std::endl;
      99                 :      83341 :   NodeManager* nm = nodeManager();
     100         [ +  + ]:      96261 :   for (auto& subTheory : d_subTheories)
     101                 :            :   {
     102                 :      12920 :     Result r = subTheory.second.postCheck(level);
     103 [ +  + ][ -  + ]:      12920 :     if (r.getStatus() == Result::UNKNOWN && level >= EFFORT_FULL)
                 [ -  + ]
     104                 :            :     {
     105                 :          0 :       d_im.setModelUnsound(IncompleteId::UNKNOWN);
     106                 :            :     }
     107         [ +  + ]:      12920 :     else if (r.getStatus() == Result::UNSAT)
     108                 :            :     {
     109 [ -  + ][ -  + ]:       2515 :       Assert(subTheory.second.inConflict());
                 [ -  - ]
     110                 :       2515 :       const Node conflict = nm->mkAnd(subTheory.second.conflict());
     111         [ +  - ]:       2515 :       Trace("ff::conflict") << "ff::conflict : " << conflict << std::endl;
     112                 :       2515 :       d_im.conflict(conflict, InferenceId::FF_LEMMA);
     113                 :       2515 :     }
     114                 :      12920 :   }
     115                 :            : #else  /* CVC5_USE_COCOA */
     116                 :            :   // We've received no facts (or we'd have crashed on notifyFact), so do nothing
     117                 :            : #endif /* CVC5_USE_COCOA */
     118                 :      83341 : }
     119                 :            : 
     120                 :      23881 : void TheoryFiniteFields::notifyFact(CVC5_UNUSED TNode atom,
     121                 :            :                                     CVC5_UNUSED bool polarity,
     122                 :            :                                     CVC5_UNUSED TNode fact,
     123                 :            :                                     CVC5_UNUSED bool isInternal)
     124                 :            : {
     125                 :            : #ifdef CVC5_USE_COCOA
     126         [ +  - ]:      47762 :   Trace("ff::check") << "ff::notifyFact : " << fact << " @ level "
     127                 :      23881 :                      << context()->getLevel() << std::endl;
     128                 :      23881 :   d_subTheories.at(atom[0].getType()).notifyFact(fact);
     129                 :            : #else  /* CVC5_USE_COCOA */
     130                 :            :   noCoCoA();
     131                 :            : #endif /* CVC5_USE_COCOA */
     132                 :      23881 : }
     133                 :            : 
     134                 :      14614 : bool TheoryFiniteFields::collectModelValues(
     135                 :            :     CVC5_UNUSED TheoryModel* m, CVC5_UNUSED const std::set<Node>& termSet)
     136                 :            : {
     137                 :            : #ifdef CVC5_USE_COCOA
     138         [ +  - ]:      14614 :   Trace("ff::model") << "Term set: " << termSet << std::endl;
     139         [ +  + ]:      14664 :   for (const auto& subTheory : d_subTheories)
     140                 :            :   {
     141         [ +  + ]:        132 :     for (const auto& entry : subTheory.second.model())
     142                 :            :     {
     143         [ +  - ]:        164 :       Trace("ff::model") << "Model entry: " << entry.first << " -> "
     144                 :         82 :                          << entry.second << std::endl;
     145         [ +  - ]:         82 :       if (termSet.count(entry.first))
     146                 :            :       {
     147                 :         82 :         bool okay = m->assertEquality(entry.first, entry.second, true);
     148 [ -  + ][ -  + ]:         82 :         AlwaysAssert(okay) << "Our model was rejected";
                 [ -  - ]
     149                 :            :       }
     150                 :            :     }
     151                 :            :   }
     152                 :            : #else  /* CVC5_USE_COCOA */
     153                 :            :   // We've received no facts (or we'd have crashed on notifyFact), so do nothing
     154                 :            : #endif /* CVC5_USE_COCOA */
     155                 :      14614 :   return true;
     156                 :            : }
     157                 :            : 
     158                 :       4390 : void TheoryFiniteFields::preRegisterWithEe(TNode node)
     159                 :            : {
     160 [ -  + ][ -  + ]:       4390 :   Assert(d_equalityEngine != nullptr);
                 [ -  - ]
     161         [ +  + ]:       4390 :   if (node.getKind() == Kind::EQUAL)
     162                 :            :   {
     163                 :       1499 :     d_state.addEqualityEngineTriggerPredicate(node);
     164                 :            :   }
     165                 :            :   else
     166                 :            :   {
     167                 :       2891 :     d_equalityEngine->addTerm(node);
     168                 :            :   }
     169                 :       4390 : }
     170                 :            : 
     171                 :       4390 : void TheoryFiniteFields::preRegisterTerm(TNode node)
     172                 :            : {
     173                 :       4390 :   preRegisterWithEe(node);
     174                 :            : #ifdef CVC5_USE_COCOA
     175         [ +  - ]:       4390 :   Trace("ff::register") << "ff::preRegisterTerm : " << node << std::endl;
     176                 :       4390 :   TypeNode ty = node.getType();
     177                 :       4390 :   TypeNode fieldTy = ty;
     178         [ +  + ]:       4390 :   if (!ty.isFiniteField())
     179                 :            :   {
     180 [ -  + ][ -  + ]:       1499 :     Assert(node.getKind() == Kind::EQUAL);
                 [ -  - ]
     181                 :       1499 :     fieldTy = node[0].getType();
     182                 :            :   }
     183         [ -  + ]:       2891 :   else if (!options().ff.ff)
     184                 :            :   {
     185                 :          0 :     std::stringstream ss;
     186                 :          0 :     ss << "Finite fields not available in this configuration, try --ff.";
     187                 :          0 :     throw SafeLogicException(ss.str());
     188                 :          0 :   }
     189         [ +  + ]:       4390 :   if (d_subTheories.count(fieldTy) == 0)
     190                 :            :   {
     191                 :        259 :     d_subTheories.try_emplace(fieldTy, d_env, d_stats.get(), ty.getFfSize());
     192                 :            :   }
     193                 :            : #else  /* CVC5_USE_COCOA */
     194                 :            :   noCoCoA();
     195                 :            : #endif /* CVC5_USE_COCOA */
     196                 :       4390 : }
     197                 :            : 
     198                 :        288 : TrustNode TheoryFiniteFields::explain(TNode n)
     199                 :            : {
     200         [ +  - ]:        288 :   Trace("ff::prop") << "explain " << n << std::endl;
     201                 :        288 :   TrustNode exp = d_im.explainLit(n);
     202 [ -  + ][ -  + ]:        288 :   AlwaysAssert(!exp.isNull());
                 [ -  - ]
     203                 :        288 :   return exp;
     204                 :          0 : }
     205                 :            : 
     206                 :            : }  // namespace ff
     207                 :            : }  // namespace theory
     208                 :            : }  // namespace cvc5::internal