GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/eager_solver.cpp Lines: 65 66 98.5 %
Date: 2021-03-22 Branches: 122 228 53.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file eager_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang, Andres Noetzli
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 The eager solver
13
 **/
14
15
#include "theory/strings/eager_solver.h"
16
17
#include "theory/strings/theory_strings_utils.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace strings {
24
25
8995
EagerSolver::EagerSolver(SolverState& state) : d_state(state) {}
26
27
8992
EagerSolver::~EagerSolver() {}
28
29
83762
void EagerSolver::eqNotifyNewClass(TNode t)
30
{
31
83762
  Kind k = t.getKind();
32
83762
  if (k == STRING_LENGTH || k == STRING_TO_CODE)
33
  {
34
24508
    eq::EqualityEngine* ee = d_state.getEqualityEngine();
35
49016
    Node r = ee->getRepresentative(t[0]);
36
24508
    EqcInfo* ei = d_state.getOrMakeEqcInfo(r);
37
24508
    if (k == STRING_LENGTH)
38
    {
39
22813
      ei->d_lengthTerm = t[0];
40
    }
41
    else
42
    {
43
1695
      ei->d_codeTerm = t[0];
44
24508
    }
45
  }
46
59254
  else if (t.isConst())
47
  {
48
23330
    if (t.getType().isStringLike())
49
    {
50
13012
      EqcInfo* ei = d_state.getOrMakeEqcInfo(t);
51
13012
      ei->d_prefixC = t;
52
13012
      ei->d_suffixC = t;
53
    }
54
  }
55
35924
  else if (k == STRING_CONCAT)
56
  {
57
6840
    addEndpointsToEqcInfo(t, t, t);
58
  }
59
83762
}
60
61
809479
void EagerSolver::eqNotifyMerge(TNode t1, TNode t2)
62
{
63
809479
  EqcInfo* e2 = d_state.getOrMakeEqcInfo(t2, false);
64
809479
  if (e2 == nullptr)
65
  {
66
589337
    return;
67
  }
68
220142
  Assert(t1.getType().isStringLike());
69
220142
  EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
70
  // add information from e2 to e1
71
220142
  if (!e2->d_lengthTerm.get().isNull())
72
  {
73
220002
    e1->d_lengthTerm.set(e2->d_lengthTerm);
74
  }
75
220142
  if (!e2->d_codeTerm.get().isNull())
76
  {
77
7381
    e1->d_codeTerm.set(e2->d_codeTerm);
78
  }
79
220142
  if (!e2->d_prefixC.get().isNull())
80
  {
81
45308
    d_state.setPendingPrefixConflictWhen(
82
45308
        e1->addEndpointConst(e2->d_prefixC, Node::null(), false));
83
  }
84
220142
  if (!e2->d_suffixC.get().isNull())
85
  {
86
73300
    d_state.setPendingPrefixConflictWhen(
87
73300
        e1->addEndpointConst(e2->d_suffixC, Node::null(), true));
88
  }
89
220142
  if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get())
90
  {
91
    e1->d_cardinalityLemK.set(e2->d_cardinalityLemK);
92
  }
93
220142
  if (!e2->d_normalizedLength.get().isNull())
94
  {
95
101
    e1->d_normalizedLength.set(e2->d_normalizedLength);
96
  }
97
}
98
99
127954
void EagerSolver::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
100
{
101
127954
  if (t1.getType().isStringLike())
102
  {
103
    // store disequalities between strings, may need to check if their lengths
104
    // are equal/disequal
105
50748
    d_state.addDisequality(t1, t2);
106
  }
107
127954
}
108
109
7693
void EagerSolver::addEndpointsToEqcInfo(Node t, Node concat, Node eqc)
110
{
111
7693
  Assert(concat.getKind() == STRING_CONCAT
112
         || concat.getKind() == REGEXP_CONCAT);
113
7693
  EqcInfo* ei = nullptr;
114
  // check each side
115
23079
  for (unsigned r = 0; r < 2; r++)
116
  {
117
15386
    unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1;
118
30772
    Node c = utils::getConstantComponent(concat[index]);
119
15386
    if (!c.isNull())
120
    {
121
3647
      if (ei == nullptr)
122
      {
123
3188
        ei = d_state.getOrMakeEqcInfo(eqc);
124
      }
125
7294
      Trace("strings-eager-pconf-debug")
126
3647
          << "New term: " << concat << " for " << t << " with prefix " << c
127
3647
          << " (" << (r == 1) << ")" << std::endl;
128
3647
      d_state.setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1));
129
    }
130
  }
131
7693
}
132
133
606809
void EagerSolver::notifyFact(TNode atom,
134
                             bool polarity,
135
                             TNode fact,
136
                             bool isInternal)
137
{
138
606809
  if (atom.getKind() == STRING_IN_REGEXP)
139
  {
140
4807
    if (polarity && atom[1].getKind() == REGEXP_CONCAT)
141
    {
142
853
      eq::EqualityEngine* ee = d_state.getEqualityEngine();
143
1706
      Node eqc = ee->getRepresentative(atom[0]);
144
853
      addEndpointsToEqcInfo(atom, atom[1], eqc);
145
    }
146
  }
147
606809
}
148
149
}  // namespace strings
150
}  // namespace theory
151
26676
}  // namespace CVC4