Branch data     Line data    Source code

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