Branch data     Line data    Source code

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