Branch data     Line data    Source code

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