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 strategy of the theory of strings.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/strings/strategy.h"
      14                 :            : 
      15                 :            : #include "options/strings_options.h"
      16                 :            : 
      17                 :            : namespace cvc5::internal {
      18                 :            : namespace theory {
      19                 :            : namespace strings {
      20                 :            : 
      21                 :         21 : std::ostream& operator<<(std::ostream& out, InferStep s)
      22                 :            : {
      23 [ +  + ][ +  + ]:         21 :   switch (s)
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
            [ +  - ][ - ]
      24                 :            :   {
      25                 :          1 :     case InferStep::NONE: out << "none"; break;
      26                 :          1 :     case InferStep::BREAK: out << "break"; break;
      27                 :          1 :     case InferStep::CHECK_INIT: out << "check_init"; break;
      28                 :          1 :     case InferStep::CHECK_CONST_EQC: out << "check_const_eqc"; break;
      29                 :          1 :     case InferStep::CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
      30                 :          1 :     case InferStep::CHECK_CYCLES: out << "check_cycles"; break;
      31                 :          1 :     case InferStep::CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
      32                 :          1 :     case InferStep::CHECK_NORMAL_FORMS_EQ_PROP:
      33                 :          1 :       out << "check_normal_forms_eq_prop";
      34                 :          1 :       break;
      35                 :          1 :     case InferStep::CHECK_NORMAL_FORMS_EQ:
      36                 :          1 :       out << "check_normal_forms_eq";
      37                 :          1 :       break;
      38                 :          1 :     case InferStep::CHECK_NORMAL_FORMS_DEQ:
      39                 :          1 :       out << "check_normal_forms_deq";
      40                 :          1 :       break;
      41                 :          1 :     case InferStep::CHECK_CODES: out << "check_codes"; break;
      42                 :          1 :     case InferStep::CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
      43                 :          1 :     case InferStep::CHECK_REGISTER_TERMS_NF:
      44                 :          1 :       out << "check_register_terms_nf";
      45                 :          1 :       break;
      46                 :          1 :     case InferStep::CHECK_EXTF_REDUCTION_EAGER:
      47                 :          1 :       out << "check_extf_reduction_eager";
      48                 :          1 :       break;
      49                 :          1 :     case InferStep::CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
      50                 :          1 :     case InferStep::CHECK_MEMBERSHIP_EAGER:
      51                 :          1 :       out << "check_membership_eager";
      52                 :          1 :       break;
      53                 :          1 :     case InferStep::CHECK_MEMBERSHIP: out << "check_membership"; break;
      54                 :          1 :     case InferStep::CHECK_CARDINALITY: out << "check_cardinality"; break;
      55                 :          1 :     case InferStep::CHECK_SEQUENCES_ARRAY_CONCAT:
      56                 :          1 :       out << "check_sequences_update_concat_terms";
      57                 :          1 :       break;
      58                 :          1 :     case InferStep::CHECK_SEQUENCES_ARRAY:
      59                 :          1 :       out << "check_sequences_array";
      60                 :          1 :       break;
      61                 :          1 :     case InferStep::CHECK_SEQUENCES_ARRAY_EAGER:
      62                 :          1 :       out << "check_sequences_array_eager";
      63                 :          1 :       break;
      64                 :          0 :     case InferStep::UNKNOWN: out << "?"; break;
      65                 :          0 :     default:
      66                 :          0 :       Unreachable();
      67                 :            :       out << "?unhandled";
      68                 :            :       break;
      69                 :            :   }
      70                 :         21 :   return out;
      71                 :            : }
      72                 :            : 
      73                 :      51016 : Strategy::Strategy(Env& env) : EnvObj(env), d_strategy_init(false) {}
      74                 :            : 
      75                 :      50668 : Strategy::~Strategy() {}
      76                 :            : 
      77                 :     916301 : bool Strategy::isStrategyInit() const { return d_strategy_init; }
      78                 :            : 
      79                 :     233862 : bool Strategy::hasStrategyEffort(Theory::Effort e) const
      80                 :            : {
      81                 :     233862 :   return d_strat_steps.find(e) != d_strat_steps.end();
      82                 :            : }
      83                 :            : 
      84                 :     105132 : std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin(
      85                 :            :     Theory::Effort e)
      86                 :            : {
      87                 :            :   std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
      88                 :     105132 :       d_strat_steps.find(e);
      89 [ -  + ][ -  + ]:     105132 :   Assert(it != d_strat_steps.end());
                 [ -  - ]
      90                 :     105132 :   return d_infer_steps.begin() + it->second.first;
      91                 :            : }
      92                 :            : 
      93                 :     105132 : std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd(
      94                 :            :     Theory::Effort e)
      95                 :            : {
      96                 :            :   std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
      97                 :     105132 :       d_strat_steps.find(e);
      98 [ -  + ][ -  + ]:     105132 :   Assert(it != d_strat_steps.end());
                 [ -  - ]
      99                 :     105132 :   return d_infer_steps.begin() + it->second.second;
     100                 :            : }
     101                 :            : 
     102                 :     780525 : void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak)
     103                 :            : {
     104                 :            :   // must run check init first
     105 [ -  + ][ -  + ]:     780525 :   Assert((s == InferStep::CHECK_INIT) == d_infer_steps.empty());
                 [ -  - ]
     106                 :     780525 :   d_infer_steps.push_back(std::pair<InferStep, int>(s, effort));
     107         [ +  - ]:     780525 :   if (addBreak)
     108                 :            :   {
     109                 :     780525 :     d_infer_steps.push_back(std::pair<InferStep, int>(InferStep::BREAK, 0));
     110                 :            :   }
     111                 :     780525 : }
     112                 :            : 
     113                 :      50442 : void Strategy::initializeStrategy()
     114                 :            : {
     115                 :            :   // initialize the strategy if not already done so
     116         [ +  + ]:      50442 :   if (!d_strategy_init)
     117                 :            :   {
     118                 :      42810 :     std::map<Theory::Effort, unsigned> step_begin;
     119                 :      42810 :     std::map<Theory::Effort, unsigned> step_end;
     120                 :      42810 :     d_strategy_init = true;
     121                 :            :     // beginning indices
     122                 :      42810 :     step_begin[Theory::EFFORT_FULL] = 0;
     123                 :            :     // add the inference steps
     124                 :      42810 :     addStrategyStep(InferStep::CHECK_INIT);
     125                 :      42810 :     addStrategyStep(InferStep::CHECK_CONST_EQC);
     126                 :      42810 :     addStrategyStep(InferStep::CHECK_EXTF_EVAL, 0);
     127         [ +  + ]:      42810 :     if (options().strings.seqArray == options::SeqArrayMode::EAGER)
     128                 :            :     {
     129                 :         71 :       addStrategyStep(InferStep::CHECK_SEQUENCES_ARRAY_EAGER);
     130                 :            :     }
     131                 :            :     // we must check cycles before using flat forms
     132                 :      42810 :     addStrategyStep(InferStep::CHECK_CYCLES);
     133         [ +  - ]:      42810 :     if (options().strings.stringFlatForms)
     134                 :            :     {
     135                 :      42810 :       addStrategyStep(InferStep::CHECK_FLAT_FORMS);
     136                 :            :     }
     137                 :      42810 :     addStrategyStep(InferStep::CHECK_EXTF_REDUCTION_EAGER);
     138                 :      42810 :     addStrategyStep(InferStep::CHECK_MEMBERSHIP_EAGER);
     139                 :      42810 :     addStrategyStep(InferStep::CHECK_NORMAL_FORMS_EQ_PROP);
     140                 :      42810 :     addStrategyStep(InferStep::CHECK_NORMAL_FORMS_EQ);
     141                 :      42810 :     addStrategyStep(InferStep::CHECK_EXTF_EVAL, 1);
     142                 :      42810 :     addStrategyStep(InferStep::CHECK_NORMAL_FORMS_DEQ);
     143                 :      42810 :     addStrategyStep(InferStep::CHECK_CODES);
     144         [ +  - ]:      42810 :     if (options().strings.stringLenNorm)
     145                 :            :     {
     146                 :      42810 :       addStrategyStep(InferStep::CHECK_LENGTH_EQC);
     147                 :            :     }
     148         [ +  + ]:      42810 :     if (options().strings.seqArray != options::SeqArrayMode::NONE)
     149                 :            :     {
     150                 :        135 :       addStrategyStep(InferStep::CHECK_SEQUENCES_ARRAY_CONCAT);
     151                 :        135 :       addStrategyStep(InferStep::CHECK_SEQUENCES_ARRAY);
     152                 :            :     }
     153         [ +  + ]:      42810 :     if (options().strings.stringExp)
     154                 :            :     {
     155                 :      26207 :       addStrategyStep(InferStep::CHECK_EXTF_REDUCTION);
     156                 :            :     }
     157                 :      42810 :     addStrategyStep(InferStep::CHECK_MEMBERSHIP);
     158                 :      42810 :     addStrategyStep(InferStep::CHECK_CARDINALITY);
     159                 :      42810 :     step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
     160         [ +  - ]:      42810 :     if (options().strings.stringModelBasedReduction)
     161                 :            :     {
     162                 :      42810 :       step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
     163                 :      42810 :       addStrategyStep(InferStep::CHECK_EXTF_EVAL, 3);
     164         [ +  + ]:      42810 :       if (options().strings.stringExp)
     165                 :            :       {
     166                 :      26207 :         addStrategyStep(InferStep::CHECK_EXTF_REDUCTION);
     167                 :            :       }
     168                 :      42810 :       addStrategyStep(InferStep::CHECK_MEMBERSHIP);
     169                 :      42810 :       step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
     170                 :            :     }
     171                 :            :     // set the beginning/ending ranges
     172         [ +  + ]:     128430 :     for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin)
     173                 :            :     {
     174                 :      85620 :       Theory::Effort e = it_begin.first;
     175                 :      85620 :       std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
     176 [ -  + ][ -  + ]:      85620 :       Assert(it_end != step_end.end());
                 [ -  - ]
     177                 :      85620 :       d_strat_steps[e] =
     178                 :     171240 :           std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
     179                 :            :     }
     180                 :      42810 :   }
     181                 :      50442 : }
     182                 :            : 
     183                 :            : }  // namespace strings
     184                 :            : }  // namespace theory
     185                 :            : }  // namespace cvc5::internal