GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/solver_state.cpp Lines: 101 106 95.3 %
Date: 2021-03-23 Branches: 156 338 46.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Mathias Preiner
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 solver state of the theory of strings.
13
 **/
14
15
#include "theory/strings/solver_state.h"
16
17
#include "theory/rewriter.h"
18
#include "theory/strings/theory_strings_utils.h"
19
#include "theory/strings/word.h"
20
21
using namespace std;
22
using namespace CVC4::context;
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace strings {
28
29
8997
SolverState::SolverState(context::Context* c,
30
                         context::UserContext* u,
31
8997
                         Valuation& v)
32
8997
    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN)
33
{
34
8997
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
35
8997
  d_false = NodeManager::currentNM()->mkConst(false);
36
8997
}
37
38
17988
SolverState::~SolverState()
39
{
40
30386
  for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo)
41
  {
42
21392
    delete it.second;
43
  }
44
8994
}
45
46
9309
const context::CDList<Node>& SolverState::getDisequalityList() const
47
{
48
9309
  return d_eeDisequalities;
49
}
50
51
50750
void SolverState::addDisequality(TNode t1, TNode t2)
52
{
53
50750
  d_eeDisequalities.push_back(t1.eqNode(t2));
54
50750
}
55
56
1209473
EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
57
{
58
1209473
  std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc);
59
1209473
  if (eqc_i != d_eqcInfo.end())
60
  {
61
598240
    return eqc_i->second;
62
  }
63
611233
  if (doMake)
64
  {
65
21392
    EqcInfo* ei = new EqcInfo(d_context);
66
21392
    d_eqcInfo[eqc] = ei;
67
21392
    return ei;
68
  }
69
589841
  return nullptr;
70
}
71
72
TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
73
74
508860
Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
75
{
76
508860
  Assert(areEqual(t, te));
77
1017720
  Node lt = utils::mkNLength(te);
78
508860
  if (hasTerm(lt))
79
  {
80
    // use own length if it exists, leads to shorter explanation
81
508294
    return lt;
82
  }
83
566
  EqcInfo* ei = getOrMakeEqcInfo(t, false);
84
1132
  Node lengthTerm = ei ? ei->d_lengthTerm : Node::null();
85
566
  if (lengthTerm.isNull())
86
  {
87
    // typically shouldnt be necessary
88
534
    lengthTerm = t;
89
  }
90
1132
  Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm
91
566
                   << std::endl;
92
566
  if (te != lengthTerm)
93
  {
94
32
    exp.push_back(te.eqNode(lengthTerm));
95
  }
96
  return Rewriter::rewrite(
97
566
      NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm));
98
}
99
100
508852
Node SolverState::getLength(Node t, std::vector<Node>& exp)
101
{
102
508852
  return getLengthExp(t, exp, t);
103
}
104
105
12352
Node SolverState::explainNonEmpty(Node s)
106
{
107
12352
  Assert(s.getType().isStringLike());
108
24704
  Node emp = Word::mkEmptyWord(s.getType());
109
12352
  if (areDisequal(s, emp))
110
  {
111
4751
    return s.eqNode(emp).negate();
112
  }
113
15202
  Node sLen = utils::mkNLength(s);
114
7601
  if (areDisequal(sLen, d_zero))
115
  {
116
7601
    return sLen.eqNode(d_zero).negate();
117
  }
118
  return Node::null();
119
}
120
121
527841
bool SolverState::isEqualEmptyWord(Node s, Node& emps)
122
{
123
1055682
  Node sr = getRepresentative(s);
124
527841
  if (sr.isConst())
125
  {
126
138334
    if (Word::getLength(sr) == 0)
127
    {
128
18237
      emps = sr;
129
18237
      return true;
130
    }
131
  }
132
509604
  return false;
133
}
134
135
62951
void SolverState::setPendingPrefixConflictWhen(Node conf)
136
{
137
62951
  if (conf.isNull() || d_pendingConflictSet.get())
138
  {
139
62606
    return;
140
  }
141
690
  InferInfo iiPrefixConf(InferenceId::STRINGS_PREFIX_CONFLICT);
142
345
  iiPrefixConf.d_conc = d_false;
143
345
  utils::flattenOp(AND, conf, iiPrefixConf.d_premises);
144
345
  setPendingConflict(iiPrefixConf);
145
}
146
147
345
void SolverState::setPendingConflict(InferInfo& ii)
148
{
149
345
  if (!d_pendingConflictSet.get())
150
  {
151
345
    d_pendingConflict = ii;
152
345
    d_pendingConflictSet.set(true);
153
  }
154
345
}
155
156
604930
bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; }
157
158
285
bool SolverState::getPendingConflict(InferInfo& ii) const
159
{
160
285
  if (d_pendingConflictSet)
161
  {
162
285
    ii = d_pendingConflict;
163
285
    return true;
164
  }
165
  return false;
166
}
167
168
5208
std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
169
                                                   TNode lit)
170
{
171
5208
  return d_valuation.entailmentCheck(mode, lit);
172
}
173
174
17021
void SolverState::separateByLength(
175
    const std::vector<Node>& n,
176
    std::map<TypeNode, std::vector<std::vector<Node>>>& cols,
177
    std::map<TypeNode, std::vector<Node>>& lts)
178
{
179
17021
  unsigned leqc_counter = 0;
180
  // map (length, type) to an equivalence class identifier
181
34042
  std::map<std::pair<Node, TypeNode>, unsigned> eqc_to_leqc;
182
  // backwards map
183
34042
  std::map<unsigned, std::pair<Node, TypeNode>> leqc_to_eqc;
184
  // Collection of eqc for each identifier. Notice that some identifiers may
185
  // not have an associated length in the mappings above, if the length of
186
  // an equivalence class is unknown.
187
34042
  std::map<unsigned, std::vector<Node> > eqc_to_strings;
188
17021
  NodeManager* nm = NodeManager::currentNM();
189
72508
  for (const Node& eqc : n)
190
  {
191
55487
    Assert(d_ee->getRepresentative(eqc) == eqc);
192
110974
    TypeNode tnEqc = eqc.getType();
193
55487
    EqcInfo* ei = getOrMakeEqcInfo(eqc, false);
194
110974
    Node lt = ei ? ei->d_lengthTerm : Node::null();
195
55487
    if (!lt.isNull())
196
    {
197
55487
      lt = nm->mkNode(STRING_LENGTH, lt);
198
110974
      Node r = d_ee->getRepresentative(lt);
199
110974
      std::pair<Node, TypeNode> lkey(r, tnEqc);
200
55487
      if (eqc_to_leqc.find(lkey) == eqc_to_leqc.end())
201
      {
202
33083
        eqc_to_leqc[lkey] = leqc_counter;
203
33083
        leqc_to_eqc[leqc_counter] = lkey;
204
33083
        leqc_counter++;
205
      }
206
55487
      eqc_to_strings[eqc_to_leqc[lkey]].push_back(eqc);
207
    }
208
    else
209
    {
210
      eqc_to_strings[leqc_counter].push_back(eqc);
211
      leqc_counter++;
212
    }
213
  }
214
50104
  for (const std::pair<const unsigned, std::vector<Node> >& p : eqc_to_strings)
215
  {
216
33083
    Assert(!p.second.empty());
217
    // get the type of the collection
218
66166
    TypeNode stn = p.second[0].getType();
219
33083
    cols[stn].emplace_back(p.second.begin(), p.second.end());
220
33083
    lts[stn].push_back(leqc_to_eqc[p.first].first);
221
  }
222
17021
}
223
224
}  // namespace strings
225
}  // namespace theory
226
26685
}  // namespace CVC4