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                 :            :  * Utility for quantifiers state.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/quantifiers_state.h"
      14                 :            : 
      15                 :            : #include "options/quantifiers_options.h"
      16                 :            : #include "theory/uf/equality_engine.h"
      17                 :            : #include "theory/uf/equality_engine_iterator.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : namespace theory {
      21                 :            : namespace quantifiers {
      22                 :            : 
      23                 :      50165 : QuantifiersState::QuantifiersState(Env& env,
      24                 :            :                                    Valuation val,
      25                 :      50165 :                                    const LogicInfo& logicInfo)
      26                 :            :     : TheoryState(env, val),
      27                 :      50165 :       d_ierCounterc(context()),
      28                 :      50165 :       d_conflictInst(context()),
      29                 :      50165 :       d_logicInfo(logicInfo),
      30                 :     100330 :       d_statistics(statisticsRegistry())
      31                 :            : {
      32                 :            :   // allow theory combination to go first, once initially
      33                 :      50165 :   d_ierCounter = 0;
      34                 :      50165 :   d_ierCounterc = d_ierCounter;
      35                 :      50165 :   d_ierCounterLc = 0;
      36                 :      50165 :   d_ierCounterLastLc = 0;
      37                 :      50165 :   d_instWhenPhase = 1
      38         [ +  - ]:      50165 :                     + (options().quantifiers.instWhenPhase < 1
      39                 :            :                            ? 1
      40                 :      50165 :                            : options().quantifiers.instWhenPhase);
      41                 :      50165 : }
      42                 :            : 
      43                 :     224113 : void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
      44                 :            : {
      45         [ +  + ]:     224113 :   if (e == Theory::EFFORT_FULL)
      46                 :            :   {
      47                 :            :     // increment if a last call happened, or already were in phase
      48         [ +  + ]:     106845 :     if (d_ierCounterLastLc != d_ierCounterLc
      49         [ +  + ]:      79366 :         || d_ierCounter % d_instWhenPhase != 0)
      50                 :            :     {
      51                 :      32923 :       d_ierCounter = d_ierCounter + 1;
      52                 :      32923 :       d_ierCounterLastLc = d_ierCounterLc;
      53                 :      32923 :       d_ierCounterc = d_ierCounterc.get() + 1;
      54                 :            :     }
      55                 :            :   }
      56         [ +  + ]:     117268 :   else if (e == Theory::EFFORT_LAST_CALL)
      57                 :            :   {
      58                 :      47738 :     d_ierCounterLc = d_ierCounterLc + 1;
      59                 :            :   }
      60                 :     224113 : }
      61                 :            : 
      62                 :     280103 : bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
      63                 :            : {
      64         [ +  - ]:     560206 :   Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
      65                 :     280103 :                         << ", " << d_ierCounterLc << std::endl;
      66                 :            :   // determine if we should perform check, based on instWhenMode
      67                 :     280103 :   bool performCheck = false;
      68         [ +  + ]:     280103 :   if (options().quantifiers.instWhenMode == options::InstWhenMode::FULL)
      69                 :            :   {
      70                 :         40 :     performCheck = (e >= Theory::EFFORT_FULL);
      71                 :            :   }
      72                 :     280063 :   else if (options().quantifiers.instWhenMode
      73         [ -  + ]:     280063 :            == options::InstWhenMode::FULL_DELAY)
      74                 :            :   {
      75                 :          0 :     performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
      76                 :            :   }
      77                 :     280063 :   else if (options().quantifiers.instWhenMode
      78         [ +  + ]:     280063 :            == options::InstWhenMode::FULL_LAST_CALL)
      79                 :            :   {
      80                 :     257639 :     performCheck =
      81         [ +  + ]:      89336 :         ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
      82 [ +  + ][ +  + ]:     346975 :          || e == Theory::EFFORT_LAST_CALL);
      83                 :            :   }
      84                 :      22424 :   else if (options().quantifiers.instWhenMode
      85         [ -  + ]:      22424 :            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
      86                 :            :   {
      87         [ -  - ]:          0 :     performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
      88         [ -  - ]:          0 :                      && d_ierCounter % d_instWhenPhase != 0)
      89 [ -  - ][ -  - ]:          0 :                     || e == Theory::EFFORT_LAST_CALL);
      90                 :            :   }
      91                 :      22424 :   else if (options().quantifiers.instWhenMode
      92         [ +  - ]:      22424 :            == options::InstWhenMode::LAST_CALL)
      93                 :            :   {
      94                 :      22424 :     performCheck = (e >= Theory::EFFORT_LAST_CALL);
      95                 :            :   }
      96                 :            :   else
      97                 :            :   {
      98                 :          0 :     performCheck = true;
      99                 :            :   }
     100         [ +  - ]:     280103 :   Trace("qstate-debug") << "...returned " << performCheck << std::endl;
     101                 :     280103 :   return performCheck;
     102                 :            : }
     103                 :            : 
     104                 :          0 : uint64_t QuantifiersState::getInstRoundDepth() const
     105                 :            : {
     106                 :          0 :   return d_ierCounterc.get();
     107                 :            : }
     108                 :            : 
     109                 :          0 : uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }
     110                 :            : 
     111                 :          0 : void QuantifiersState::debugPrintEqualityEngine(const char* c) const
     112                 :            : {
     113                 :          0 :   bool traceEnabled = TraceIsOn(c);
     114         [ -  - ]:          0 :   if (!traceEnabled)
     115                 :            :   {
     116                 :          0 :     return;
     117                 :            :   }
     118                 :          0 :   eq::EqualityEngine* ee = getEqualityEngine();
     119                 :          0 :   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
     120                 :          0 :   std::map<TypeNode, uint64_t> tnum;
     121         [ -  - ]:          0 :   while (!eqcs_i.isFinished())
     122                 :            :   {
     123                 :          0 :     tnum[(*eqcs_i).getType()]++;
     124                 :          0 :     ++eqcs_i;
     125                 :            :   }
     126                 :          0 :   Trace(c) << ee->debugPrintEqc() << std::endl;
     127         [ -  - ]:          0 :   for (const std::pair<const TypeNode, uint64_t>& t : tnum)
     128                 :            :   {
     129         [ -  - ]:          0 :     Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
     130                 :            :   }
     131                 :          0 : }
     132                 :            : 
     133                 :      73862 : const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
     134                 :            : 
     135                 :     559905 : QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }
     136                 :            : 
     137                 :       3656 : void QuantifiersState::notifyConflictingInst() { d_conflictInst = true; }
     138                 :            : 
     139                 :            : }  // namespace quantifiers
     140                 :            : }  // namespace theory
     141                 :            : }  // namespace cvc5::internal