GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/normal_form.cpp Lines: 84 84 100.0 %
Date: 2021-03-22 Branches: 150 342 43.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file normal_form.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Gereon Kremer
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 normal form data structure for the theory of
13
 **  strings.
14
 **/
15
16
#include "theory/strings/normal_form.h"
17
18
#include "options/strings_options.h"
19
#include "theory/rewriter.h"
20
#include "theory/strings/theory_strings_utils.h"
21
#include "theory/strings/word.h"
22
23
using namespace std;
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
namespace theory {
28
namespace strings {
29
30
103332
void NormalForm::init(Node base)
31
{
32
103332
  Assert(base.getType().isStringLike());
33
103332
  Assert(base.getKind() != STRING_CONCAT);
34
103332
  d_base = base;
35
103332
  d_nf.clear();
36
103332
  d_isRev = false;
37
103332
  d_exp.clear();
38
103332
  d_expDep.clear();
39
40
  // add to normal form
41
103332
  if (!base.isConst() || Word::getLength(base) > 0)
42
  {
43
93906
    d_nf.push_back(base);
44
  }
45
103332
}
46
47
38212
void NormalForm::reverse()
48
{
49
38212
  std::reverse(d_nf.begin(), d_nf.end());
50
38212
  d_isRev = !d_isRev;
51
38212
}
52
53
4712
void NormalForm::splitConstant(unsigned index, Node c1, Node c2)
54
{
55
4712
  Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
56
             STRING_CONCAT, d_isRev ? c2 : c1, d_isRev ? c1 : c2))
57
         == d_nf[index]);
58
4712
  d_nf.insert(d_nf.begin() + index + 1, c2);
59
4712
  d_nf[index] = c1;
60
  // update the dependency indices
61
  // notice this is not critical for soundness: not doing the below incrementing
62
  // will only lead to overapproximating when antecedants are required in
63
  // explanations
64
9654
  for (const std::pair<const Node, std::map<bool, unsigned> >& pe : d_expDep)
65
  {
66
14826
    for (const auto& pep : pe.second)
67
    {
68
      // See if this can be incremented: it can if this literal is not relevant
69
      // to the current index, and hence it is not relevant for both c1 and c2.
70
9884
      Assert(pep.second >= 0 && pep.second <= d_nf.size());
71
9884
      bool increment = (pep.first == d_isRev)
72
14826
                           ? pep.second > index
73
14826
                           : (d_nf.size() - 1 - pep.second) < index;
74
9884
      if (increment)
75
      {
76
3261
        d_expDep[pe.first][pep.first] = pep.second + 1;
77
      }
78
    }
79
  }
80
4712
}
81
82
328835
void NormalForm::addToExplanation(Node exp,
83
                                  unsigned new_val,
84
                                  unsigned new_rev_val)
85
{
86
328835
  Assert(!exp.isConst());
87
328835
  if (std::find(d_exp.begin(), d_exp.end(), exp) == d_exp.end())
88
  {
89
327637
    d_exp.push_back(exp);
90
  }
91
986505
  for (unsigned k = 0; k < 2; k++)
92
  {
93
657670
    unsigned val = k == 0 ? new_val : new_rev_val;
94
657670
    std::map<bool, unsigned>::iterator itned = d_expDep[exp].find(k == 1);
95
657670
    if (itned == d_expDep[exp].end())
96
    {
97
1310548
      Trace("strings-process-debug")
98
655274
          << "Deps : set dependency on " << exp << " to " << val
99
655274
          << " isRev=" << (k == 0) << std::endl;
100
655274
      d_expDep[exp][k == 1] = val;
101
    }
102
    else
103
    {
104
4792
      Trace("strings-process-debug")
105
2396
          << "Deps : Multiple dependencies on " << exp << " : " << itned->second
106
2396
          << " " << val << " isRev=" << (k == 0) << std::endl;
107
      // if we already have a dependency (in the case of non-linear string
108
      // equalities), it is min/max
109
2396
      bool cmp = val > itned->second;
110
2396
      if (cmp == (k == 1))
111
      {
112
1198
        d_expDep[exp][k == 1] = val;
113
      }
114
    }
115
  }
116
328835
}
117
118
23628
void NormalForm::getExplanation(int index, std::vector<Node>& curr_exp)
119
{
120
44682
  if (index == -1 || !options::stringMinPrefixExplain())
121
  {
122
2574
    curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end());
123
2574
    return;
124
  }
125
87880
  for (const Node& exp : d_exp)
126
  {
127
66826
    int dep = static_cast<int>(d_expDep[exp][d_isRev]);
128
66826
    if (dep <= index)
129
    {
130
38988
      curr_exp.push_back(exp);
131
38988
      Trace("strings-explain-prefix-debug") << "  include : ";
132
    }
133
    else
134
    {
135
27838
      Trace("strings-explain-prefix-debug") << "  exclude : ";
136
    }
137
66826
    Trace("strings-explain-prefix-debug") << exp << std::endl;
138
  }
139
}
140
141
8000
Node NormalForm::collectConstantStringAt(size_t& index)
142
{
143
16000
  std::vector<Node> c;
144
20910
  while (d_nf.size() > index && d_nf[index].isConst())
145
  {
146
6455
    c.push_back(d_nf[index]);
147
6455
    index++;
148
  }
149
8000
  if (!c.empty())
150
  {
151
5260
    if (d_isRev)
152
    {
153
3038
      std::reverse(c.begin(), c.end());
154
    }
155
10520
    Node cc = Rewriter::rewrite(utils::mkConcat(c, c[0].getType()));
156
5260
    Assert(cc.isConst());
157
5260
    return cc;
158
  }
159
  else
160
  {
161
2740
    return Node::null();
162
  }
163
}
164
165
11814
void NormalForm::getExplanationForPrefixEq(NormalForm& nfi,
166
                                           NormalForm& nfj,
167
                                           int index_i,
168
                                           int index_j,
169
                                           std::vector<Node>& curr_exp)
170
{
171
11814
  Assert(nfi.d_isRev == nfj.d_isRev);
172
23628
  Trace("strings-explain-prefix")
173
11814
      << "Get explanation for prefix " << index_i << ", " << index_j
174
11814
      << ", reverse = " << nfi.d_isRev << std::endl;
175
  // get explanations
176
11814
  nfi.getExplanation(index_i, curr_exp);
177
11814
  nfj.getExplanation(index_j, curr_exp);
178
23628
  Trace("strings-explain-prefix")
179
23628
      << "Included " << curr_exp.size() << " / "
180
11814
      << (nfi.d_exp.size() + nfj.d_exp.size()) << std::endl;
181
  // add explanation for why they are equal
182
23628
  Node eq = nfi.d_base.eqNode(nfj.d_base);
183
11814
  curr_exp.push_back(eq);
184
11814
}
185
186
}  // namespace strings
187
}  // namespace theory
188
47730
}  // namespace CVC4