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 an enumerative instantiation strategy.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/quantifiers/inst_strategy_enumerative.h"
      14                 :            : 
      15                 :            : #include "options/quantifiers_options.h"
      16                 :            : #include "theory/quantifiers/instantiate.h"
      17                 :            : #include "theory/quantifiers/relevant_domain.h"
      18                 :            : #include "theory/quantifiers/term_database.h"
      19                 :            : #include "theory/quantifiers/term_tuple_enumerator.h"
      20                 :            : #include "theory/quantifiers/term_util.h"
      21                 :            : 
      22                 :            : using namespace cvc5::internal::kind;
      23                 :            : using namespace cvc5::context;
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : namespace theory {
      27                 :            : namespace quantifiers {
      28                 :            : 
      29                 :        330 : InstStrategyEnum::InstStrategyEnum(Env& env,
      30                 :            :                                    QuantifiersState& qs,
      31                 :            :                                    QuantifiersInferenceManager& qim,
      32                 :            :                                    QuantifiersRegistry& qr,
      33                 :            :                                    TermRegistry& tr,
      34                 :        330 :                                    RelevantDomain* rd)
      35                 :        330 :     : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_enumInstLimit(-1)
      36                 :            : {
      37                 :        330 : }
      38                 :        324 : void InstStrategyEnum::presolve()
      39                 :            : {
      40                 :        324 :   d_enumInstLimit = options().quantifiers.enumInstLimit;
      41                 :        324 : }
      42                 :      18787 : bool InstStrategyEnum::needsCheck(Theory::Effort e)
      43                 :            : {
      44         [ -  + ]:      18787 :   if (d_enumInstLimit == 0)
      45                 :            :   {
      46                 :          0 :     return false;
      47                 :            :   }
      48         [ +  + ]:      18787 :   if (options().quantifiers.enumInstInterleave)
      49                 :            :   {
      50                 :            :     // if interleaved, we run at the same time as E-matching
      51         [ +  + ]:         21 :     if (d_qstate.getInstWhenNeedsCheck(e))
      52                 :            :     {
      53                 :          7 :       return true;
      54                 :            :     }
      55                 :            :   }
      56         [ +  + ]:      18780 :   if (options().quantifiers.enumInst)
      57                 :            :   {
      58         [ +  + ]:      18766 :     if (e >= Theory::EFFORT_LAST_CALL)
      59                 :            :     {
      60                 :       1139 :       return true;
      61                 :            :     }
      62                 :            :   }
      63                 :      17641 :   return false;
      64                 :            : }
      65                 :            : 
      66                 :       3671 : void InstStrategyEnum::reset_round(CVC5_UNUSED Theory::Effort e) {}
      67                 :       3665 : void InstStrategyEnum::check(CVC5_UNUSED Theory::Effort e, QEffort quant_e)
      68                 :            : {
      69                 :       3665 :   bool doCheck = false;
      70                 :       3665 :   bool fullEffort = false;
      71         [ +  - ]:       3665 :   if (d_enumInstLimit != 0)
      72                 :            :   {
      73         [ +  + ]:       3665 :     if (options().quantifiers.enumInstInterleave)
      74                 :            :     {
      75                 :            :       // we only add when interleaved with other strategies
      76 [ +  + ][ +  - ]:         14 :       doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
      77                 :            :     }
      78 [ +  + ][ +  - ]:       3665 :     if (options().quantifiers.enumInst && !doCheck)
                 [ +  + ]
      79                 :            :     {
      80         [ +  + ]:       3651 :       if (!d_qstate.getValuation().needCheck())
      81                 :            :       {
      82                 :       2467 :         doCheck = quant_e == QEFFORT_LAST_CALL;
      83                 :       2467 :         fullEffort = true;
      84                 :            :       }
      85                 :            :     }
      86                 :            :   }
      87         [ +  + ]:       3665 :   if (!doCheck)
      88                 :            :   {
      89                 :       3258 :     return;
      90                 :            :   }
      91 [ -  + ][ -  + ]:        407 :   Assert(!d_qstate.isInConflict());
                 [ -  - ]
      92                 :        407 :   beginCallDebug();
      93         [ +  - ]:        407 :   unsigned rstart = options().quantifiers.enumInstRd ? 0 : 1;
      94         [ +  + ]:        407 :   unsigned rend = fullEffort ? 1 : rstart;
      95                 :        407 :   unsigned addedLemmas = 0;
      96                 :            :   // First try in relevant domain of all quantified formulas, if no
      97                 :            :   // instantiations exist, try arbitrary ground terms.
      98                 :            :   // Notice that this stratification of effort levels makes it so that some
      99                 :            :   // quantified formulas may not be instantiated (if they have no instances
     100                 :            :   // at effort level r=0 but another quantified formula does). We prefer
     101                 :            :   // this stratification since effort level r=1 may be highly expensive in the
     102                 :            :   // case where we have a quantified formula with many entailed instances.
     103                 :        407 :   FirstOrderModel* fm = d_treg.getModel();
     104                 :        407 :   unsigned nquant = fm->getNumAssertedQuantifiers();
     105                 :        407 :   std::map<Node, bool> alreadyProc;
     106         [ +  + ]:       1174 :   for (unsigned r = rstart; r <= rend; r++)
     107                 :            :   {
     108 [ -  + ][ -  - ]:        787 :     if (d_rd || r > 0)
     109                 :            :     {
     110         [ +  + ]:        787 :       if (r == 0)
     111                 :            :       {
     112         [ +  - ]:        407 :         Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
     113         [ +  - ]:        407 :         Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
     114                 :        407 :         d_rd->compute();
     115         [ +  - ]:        407 :         Trace("inst-alg-debug") << "...finished" << std::endl;
     116                 :            :       }
     117                 :            :       else
     118                 :            :       {
     119         [ +  - ]:        380 :         Trace("inst-alg") << "-> Ground term instantiate..." << std::endl;
     120                 :            :       }
     121         [ +  + ]:       5658 :       for (unsigned i = 0; i < nquant; i++)
     122                 :            :       {
     123                 :       4871 :         Node q = fm->getAssertedQuantifier(i, true);
     124         [ -  - ]:       4871 :         bool doProcess = d_qreg.hasOwnership(q, this)
     125 [ +  - ][ +  - ]:       9699 :                          && fm->isQuantifierActive(q)
                 [ -  - ]
     126 [ +  + ][ +  + ]:       9699 :                          && alreadyProc.find(q) == alreadyProc.end();
                 [ +  + ]
     127         [ +  + ]:       4871 :         if (doProcess)
     128                 :            :         {
     129         [ +  + ]:       4275 :           if (process(q, fullEffort, r == 0))
     130                 :            :           {
     131                 :            :             // don't need to mark this if we are not stratifying
     132         [ +  + ]:       2095 :             if (!options().quantifiers.enumInstStratify)
     133                 :            :             {
     134                 :       1093 :               alreadyProc[q] = true;
     135                 :            :             }
     136                 :            :             // added lemma
     137                 :       2095 :             addedLemmas++;
     138                 :            :           }
     139         [ -  + ]:       4275 :           if (d_qstate.isInConflict())
     140                 :            :           {
     141                 :          0 :             break;
     142                 :            :           }
     143                 :            :         }
     144         [ +  - ]:       4871 :       }
     145                 :        787 :       if (d_qstate.isInConflict()
     146 [ +  - ][ +  + ]:        787 :           || (addedLemmas > 0 && options().quantifiers.enumInstStratify))
         [ +  + ][ +  + ]
     147                 :            :       {
     148                 :            :         // we break if we are in conflict, or if we added any lemma at this
     149                 :            :         // effort level and we stratify effort levels.
     150                 :         20 :         break;
     151                 :            :       }
     152                 :            :     }
     153                 :            :   }
     154                 :        407 :   endCallDebug();
     155         [ -  + ]:        407 :   if (d_enumInstLimit > 0)
     156                 :            :   {
     157                 :          0 :     d_enumInstLimit--;
     158                 :            :   }
     159                 :        407 : }
     160                 :            : 
     161                 :          0 : std::string InstStrategyEnum::identify() const { return "enum-inst"; }
     162                 :            : 
     163                 :       4275 : bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
     164                 :            : {
     165                 :            :   // ignore if constant true (rare case of non-standard quantifier whose body
     166                 :            :   // is rewritten to true)
     167                 :       4275 :   if (quantifier[1].isConst() && quantifier[1].getConst<bool>())
     168                 :            :   {
     169                 :          0 :     return false;
     170                 :            :   }
     171                 :            : 
     172                 :       4275 :   Instantiate* ie = d_qim.getInstantiate();
     173                 :            :   TermTupleEnumeratorEnv ttec;
     174                 :       4275 :   ttec.d_fullEffort = fullEffort;
     175                 :       4275 :   ttec.d_increaseSum = options().quantifiers.enumInstSum;
     176                 :       4275 :   ttec.d_tr = &d_treg;
     177                 :            :   // make the enumerator, which is either relevant domain or term database
     178                 :            :   // based on the flag isRd.
     179                 :            :   std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
     180         [ -  - ]:       6066 :       isRd ? mkTermTupleEnumeratorRd(quantifier, &ttec, d_rd)
     181 [ +  + ][ +  + ]:      11583 :            : mkTermTupleEnumerator(quantifier, &ttec, d_qstate));
         [ +  + ][ -  - ]
     182                 :       4275 :   std::vector<Node> terms;
     183                 :       4275 :   std::vector<bool> failMask;
     184         [ +  + ]:      13242 :   for (enumerator->init(); enumerator->hasNext();)
     185                 :            :   {
     186         [ -  + ]:      11062 :     if (d_qstate.isInConflict())
     187                 :            :     {
     188                 :            :       // could be conflicting for an internal reason
     189                 :          0 :       return false;
     190                 :            :     }
     191                 :      11062 :     enumerator->next(terms);
     192                 :            :     // try instantiation
     193                 :      11062 :     failMask.clear();
     194                 :            :     /* if (ie->addInstantiation(quantifier, terms)) */
     195         [ +  + ]:      11062 :     if (ie->addInstantiationExpFail(
     196                 :            :             quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM))
     197                 :            :     {
     198         [ +  - ]:       2095 :       Trace("inst-alg-rd") << "Success!" << std::endl;
     199                 :       2095 :       return true;
     200                 :            :     }
     201                 :            :     else
     202                 :            :     {
     203                 :       8967 :       enumerator->failureReason(failMask);
     204                 :            :     }
     205                 :            :   }
     206                 :       2180 :   return false;
     207                 :            :   // TODO : term enumerator instantiation?
     208                 :       4275 : }
     209                 :            : 
     210                 :            : }  // namespace quantifiers
     211                 :            : }  // namespace theory
     212                 :            : }  // namespace cvc5::internal