GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/strategy.cpp Lines: 58 82 70.7 %
Date: 2021-03-22 Branches: 87 248 35.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strategy.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Implementation of the strategy of the theory of strings.
13
 **/
14
15
#include "theory/strings/strategy.h"
16
17
#include "options/strings_options.h"
18
19
namespace CVC4 {
20
namespace theory {
21
namespace strings {
22
23
std::ostream& operator<<(std::ostream& out, InferStep s)
24
{
25
  switch (s)
26
  {
27
    case BREAK: out << "break"; break;
28
    case CHECK_INIT: out << "check_init"; break;
29
    case CHECK_CONST_EQC: out << "check_const_eqc"; break;
30
    case CHECK_EXTF_EVAL: out << "check_extf_eval"; break;
31
    case CHECK_CYCLES: out << "check_cycles"; break;
32
    case CHECK_FLAT_FORMS: out << "check_flat_forms"; break;
33
    case CHECK_NORMAL_FORMS_EQ: out << "check_normal_forms_eq"; break;
34
    case CHECK_NORMAL_FORMS_DEQ: out << "check_normal_forms_deq"; break;
35
    case CHECK_CODES: out << "check_codes"; break;
36
    case CHECK_LENGTH_EQC: out << "check_length_eqc"; break;
37
    case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break;
38
    case CHECK_MEMBERSHIP: out << "check_membership"; break;
39
    case CHECK_CARDINALITY: out << "check_cardinality"; break;
40
    default: out << "?"; break;
41
  }
42
  return out;
43
}
44
45
8995
Strategy::Strategy() : d_strategy_init(false) {}
46
47
8992
Strategy::~Strategy() {}
48
49
261321
bool Strategy::isStrategyInit() const { return d_strategy_init; }
50
51
65854
bool Strategy::hasStrategyEffort(Theory::Effort e) const
52
{
53
65854
  return d_strat_steps.find(e) != d_strat_steps.end();
54
}
55
56
25148
std::vector<std::pair<InferStep, int> >::iterator Strategy::stepBegin(
57
    Theory::Effort e)
58
{
59
  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
60
25148
      d_strat_steps.find(e);
61
25148
  Assert(it != d_strat_steps.end());
62
25148
  return d_infer_steps.begin() + it->second.first;
63
}
64
65
25148
std::vector<std::pair<InferStep, int> >::iterator Strategy::stepEnd(
66
    Theory::Effort e)
67
{
68
  std::map<Theory::Effort, std::pair<unsigned, unsigned> >::const_iterator it =
69
25148
      d_strat_steps.find(e);
70
25148
  Assert(it != d_strat_steps.end());
71
25148
  return d_infer_steps.begin() + it->second.second;
72
}
73
74
112218
void Strategy::addStrategyStep(InferStep s, int effort, bool addBreak)
75
{
76
  // must run check init first
77
112218
  Assert((s == CHECK_INIT) == d_infer_steps.empty());
78
112218
  d_infer_steps.push_back(std::pair<InferStep, int>(s, effort));
79
112218
  if (addBreak)
80
  {
81
112218
    d_infer_steps.push_back(std::pair<InferStep, int>(BREAK, 0));
82
  }
83
112218
}
84
85
12416
void Strategy::initializeStrategy()
86
{
87
  // initialize the strategy if not already done so
88
12416
  if (!d_strategy_init)
89
  {
90
17184
    std::map<Theory::Effort, unsigned> step_begin;
91
17184
    std::map<Theory::Effort, unsigned> step_end;
92
8592
    d_strategy_init = true;
93
    // beginning indices
94
8592
    step_begin[Theory::EFFORT_FULL] = 0;
95
25780
    if (options::stringEager())
96
    {
97
2
      step_begin[Theory::EFFORT_STANDARD] = 0;
98
    }
99
    // add the inference steps
100
8592
    addStrategyStep(CHECK_INIT);
101
8592
    addStrategyStep(CHECK_CONST_EQC);
102
8592
    addStrategyStep(CHECK_EXTF_EVAL, 0);
103
    // we must check cycles before using flat forms
104
8592
    addStrategyStep(CHECK_CYCLES);
105
17184
    if (options::stringFlatForms())
106
    {
107
8592
      addStrategyStep(CHECK_FLAT_FORMS);
108
    }
109
8592
    addStrategyStep(CHECK_EXTF_REDUCTION, 1);
110
8592
    if (options::stringEager())
111
    {
112
      // do only the above inferences at standard effort, if applicable
113
2
      step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1;
114
    }
115
53370
    if (!options::stringEagerLen())
116
    {
117
      addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
118
    }
119
8592
    addStrategyStep(CHECK_NORMAL_FORMS_EQ);
120
8592
    addStrategyStep(CHECK_EXTF_EVAL, 1);
121
17184
    if (!options::stringEagerLen() && options::stringLenNorm())
122
    {
123
      addStrategyStep(CHECK_LENGTH_EQC, 0, false);
124
      addStrategyStep(CHECK_REGISTER_TERMS_NF);
125
    }
126
8592
    addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
127
8592
    addStrategyStep(CHECK_CODES);
128
8592
    if (options::stringEagerLen() && options::stringLenNorm())
129
    {
130
8592
      addStrategyStep(CHECK_LENGTH_EQC);
131
    }
132
15666
    if (options::stringExp() && !options::stringGuessModel())
133
    {
134
522
      addStrategyStep(CHECK_EXTF_REDUCTION, 2);
135
    }
136
8592
    addStrategyStep(CHECK_MEMBERSHIP);
137
8592
    addStrategyStep(CHECK_CARDINALITY);
138
8592
    step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
139
8592
    if (options::stringExp() && options::stringGuessModel())
140
    {
141
      step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
142
      // these two steps are run in parallel
143
      addStrategyStep(CHECK_EXTF_REDUCTION, 2, false);
144
      addStrategyStep(CHECK_EXTF_EVAL, 3);
145
      step_end[Theory::EFFORT_LAST_CALL] = d_infer_steps.size() - 1;
146
    }
147
    // set the beginning/ending ranges
148
17186
    for (const std::pair<const Theory::Effort, unsigned>& it_begin : step_begin)
149
    {
150
8594
      Theory::Effort e = it_begin.first;
151
8594
      std::map<Theory::Effort, unsigned>::iterator it_end = step_end.find(e);
152
8594
      Assert(it_end != step_end.end());
153
8594
      d_strat_steps[e] =
154
17188
          std::pair<unsigned, unsigned>(it_begin.second, it_end->second);
155
    }
156
  }
157
12416
}
158
159
}  // namespace strings
160
}  // namespace theory
161
112900
}  // namespace CVC4