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                 :            :  * Implementation of the inference manager for the theory of strings.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/arith/inference_manager.h"
      14                 :            : 
      15                 :            : #include "options/arith_options.h"
      16                 :            : #include "theory/arith/theory_arith.h"
      17                 :            : #include "theory/rewriter.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : namespace arith {
      22                 :            : 
      23                 :      50213 : InferenceManager::InferenceManager(Env& env, TheoryArith& ta, TheoryState& s)
      24                 :            :     : InferenceManagerBuffered(env, ta, s, "theory::arith::"),
      25                 :            :       // currently must track propagated literals if using the equality solver
      26                 :      50213 :       d_trackPropLits(options().arith.arithEqSolver),
      27                 :     100426 :       d_propLits(context())
      28                 :            : {
      29                 :      50213 : }
      30                 :            : 
      31                 :      54094 : void InferenceManager::addPendingLemma(std::unique_ptr<SimpleTheoryLemma> lemma,
      32                 :            :                                        bool isWaiting)
      33                 :            : {
      34         [ +  - ]:     108188 :   Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node
      35         [ -  - ]:      54094 :                          << (isWaiting ? " as waiting" : "") << std::endl;
      36         [ +  + ]:      54094 :   if (hasCachedLemma(lemma->d_node, lemma->d_property))
      37                 :            :   {
      38                 :       1008 :     return;
      39                 :            :   }
      40         [ -  + ]:      53086 :   if (isEntailedFalse(*lemma))
      41                 :            :   {
      42         [ -  - ]:          0 :     if (isWaiting)
      43                 :            :     {
      44                 :          0 :       d_waitingLem.clear();
      45                 :            :     }
      46                 :            :     else
      47                 :            :     {
      48                 :          0 :       d_pendingLem.clear();
      49                 :          0 :       d_theoryState.notifyInConflict();
      50                 :            :     }
      51                 :            :   }
      52         [ +  + ]:      53086 :   if (isWaiting)
      53                 :            :   {
      54                 :      10929 :     d_waitingLem.emplace_back(std::move(lemma));
      55                 :            :   }
      56                 :            :   else
      57                 :            :   {
      58                 :      42157 :     d_pendingLem.emplace_back(std::move(lemma));
      59                 :            :   }
      60                 :            : }
      61                 :      11802 : void InferenceManager::addPendingLemma(const SimpleTheoryLemma& lemma,
      62                 :            :                                        bool isWaiting)
      63                 :            : {
      64                 :      11802 :   addPendingLemma(
      65                 :      23604 :       std::unique_ptr<SimpleTheoryLemma>(new SimpleTheoryLemma(lemma)),
      66                 :            :       isWaiting);
      67                 :      11802 : }
      68                 :      42292 : void InferenceManager::addPendingLemma(const Node& lemma,
      69                 :            :                                        InferenceId inftype,
      70                 :            :                                        ProofGenerator* pg,
      71                 :            :                                        bool isWaiting,
      72                 :            :                                        LemmaProperty p)
      73                 :            : {
      74                 :      84584 :   addPendingLemma(std::unique_ptr<SimpleTheoryLemma>(
      75                 :      42292 :                       new SimpleTheoryLemma(inftype, lemma, p, pg)),
      76                 :            :                   isWaiting);
      77                 :      42292 : }
      78                 :            : 
      79                 :       2491 : void InferenceManager::flushWaitingLemmas()
      80                 :            : {
      81         [ +  + ]:       7759 :   for (auto& lem : d_waitingLem)
      82                 :            :   {
      83         [ +  - ]:      10536 :     Trace("arith::infman") << "Flush waiting lemma to pending: "
      84                 :       5268 :                            << lem->getId() << " " << lem->d_node
      85                 :       5268 :                            << std::endl;
      86                 :       5268 :     d_pendingLem.emplace_back(std::move(lem));
      87                 :            :   }
      88                 :       2491 :   d_waitingLem.clear();
      89                 :       2491 : }
      90                 :     172017 : void InferenceManager::clearWaitingLemmas()
      91                 :            : {
      92                 :     172017 :   d_waitingLem.clear();
      93                 :     172017 : }
      94                 :            : 
      95                 :      22142 : bool InferenceManager::hasUsed() const
      96                 :            : {
      97 [ +  + ][ +  + ]:      22142 :   return hasSent() || hasPending();
      98                 :            : }
      99                 :            : 
     100                 :        657 : bool InferenceManager::hasWaitingLemma() const
     101                 :            : {
     102                 :        657 :   return !d_waitingLem.empty();
     103                 :            : }
     104                 :            : 
     105                 :       3001 : std::size_t InferenceManager::numWaitingLemmas() const
     106                 :            : {
     107                 :       3001 :   return d_waitingLem.size();
     108                 :            : }
     109                 :            : 
     110                 :      54094 : bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
     111                 :            : {
     112                 :      54094 :   Node rewritten = rewrite(lem);
     113                 :     108188 :   return TheoryInferenceManager::hasCachedLemma(rewritten, p);
     114                 :      54094 : }
     115                 :            : 
     116                 :     318509 : bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
     117                 :            : {
     118                 :     318509 :   Node rewritten = rewrite(lem);
     119                 :     637018 :   return TheoryInferenceManager::cacheLemma(rewritten, p);
     120                 :     318509 : }
     121                 :            : 
     122                 :      53086 : bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
     123                 :            : {
     124         [ +  + ]:      53086 :   if (options().arith.nlExtEntailConflicts)
     125                 :            :   {
     126                 :         14 :     Node ch_lemma = lem.d_node.negate();
     127                 :         14 :     ch_lemma = rewrite(ch_lemma);
     128         [ +  - ]:         28 :     Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
     129                 :         14 :                                << ch_lemma << "..." << std::endl;
     130                 :            : 
     131                 :         14 :     std::pair<bool, Node> et = d_theory.getValuation().entailmentCheck(
     132                 :         14 :         options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
     133         [ +  - ]:         28 :     Trace("arith-inf-manager") << "entailment test result : " << et.first << " "
     134                 :         14 :                                << et.second << std::endl;
     135         [ -  + ]:         14 :     if (et.first)
     136                 :            :     {
     137         [ -  - ]:          0 :       Trace("arith-inf-manager")
     138                 :          0 :           << "*** Lemma entailed to be in conflict : " << lem.d_node
     139                 :          0 :           << std::endl;
     140                 :          0 :       return true;
     141                 :            :     }
     142 [ +  - ][ +  - ]:         14 :   }
     143                 :      53086 :   return false;
     144                 :            : }
     145                 :            : 
     146                 :    2564941 : bool InferenceManager::propagateLit(TNode lit)
     147                 :            : {
     148         [ +  + ]:    2564941 :   if (d_trackPropLits)
     149                 :            :   {
     150                 :       1902 :     d_propLits.insert(lit);
     151                 :            :   }
     152                 :    2564941 :   return TheoryInferenceManager::propagateLit(lit);
     153                 :            : }
     154                 :            : 
     155                 :        293 : bool InferenceManager::hasPropagated(TNode lit) const
     156                 :            : {
     157 [ -  + ][ -  + ]:        293 :   Assert(d_trackPropLits);
                 [ -  - ]
     158                 :        293 :   return d_propLits.find(lit) != d_propLits.end();
     159                 :            : }
     160                 :            : 
     161                 :            : }  // namespace arith
     162                 :            : }  // namespace theory
     163                 :            : }  // namespace cvc5::internal