GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/eqc_info.cpp Lines: 57 57 100.0 %
Date: 2021-03-22 Branches: 148 332 44.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file eqc_info.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tianyi Liang
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 equivalence class info for the theory of strings
13
 **/
14
15
#include "theory/strings/eqc_info.h"
16
17
#include "theory/strings/theory_strings_utils.h"
18
#include "theory/strings/word.h"
19
20
using namespace std;
21
using namespace CVC4::context;
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace strings {
27
28
21372
EqcInfo::EqcInfo(context::Context* c)
29
    : d_lengthTerm(c),
30
      d_codeTerm(c),
31
      d_cardinalityLemK(c),
32
      d_normalizedLength(c),
33
      d_prefixC(c),
34
21372
      d_suffixC(c)
35
{
36
21372
}
37
38
62951
Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
39
{
40
  // check conflict
41
125902
  Node prev = isSuf ? d_suffixC : d_prefixC;
42
62951
  if (!prev.isNull())
43
  {
44
113274
    Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
45
56637
                                       << " post=" << isSuf << std::endl;
46
56845
    Node prevC = utils::getConstantEndpoint(prev, isSuf);
47
56637
    Assert(!prevC.isNull());
48
56637
    Assert(prevC.isConst());
49
56637
    if (c.isNull())
50
    {
51
56447
      c = utils::getConstantEndpoint(t, isSuf);
52
56447
      Assert(!c.isNull());
53
    }
54
56637
    Assert(c.isConst());
55
56637
    bool conflict = false;
56
    // if the constant prefixes are different
57
56637
    if (c != prevC)
58
    {
59
      // conflicts between constants should be handled by equality engine
60
15233
      Assert(!t.isConst() || !prev.isConst());
61
30466
      Trace("strings-eager-pconf-debug")
62
15233
          << "Check conflict constants " << prevC << ", " << c << std::endl;
63
15233
      size_t pvs = Word::getLength(prevC);
64
15233
      size_t cvs = Word::getLength(c);
65
30358
      if (pvs == cvs || (pvs > cvs && t.isConst())
66
30358
          || (cvs > pvs && prev.isConst()))
67
      {
68
        // If equal length, cannot be equal due to node check above.
69
        // If one is fully constant and has less length than the other, then the
70
        // other will not fit and we are in conflict.
71
271
        conflict = true;
72
      }
73
      else
74
      {
75
29924
        Node larges = pvs > cvs ? prevC : c;
76
29924
        Node smalls = pvs > cvs ? c : prevC;
77
14962
        if (isSuf)
78
        {
79
9391
          conflict = !Word::hasSuffix(larges, smalls);
80
        }
81
        else
82
        {
83
5571
          conflict = !Word::hasPrefix(larges, smalls);
84
        }
85
      }
86
15233
      if (!conflict && (pvs > cvs || prev.isConst()))
87
      {
88
        // current is subsumed, either shorter prefix or the other is a full
89
        // constant
90
14610
        return Node::null();
91
      }
92
    }
93
41404
    else if (!t.isConst())
94
    {
95
      // current is subsumed since the other may be a full constant
96
41404
      return Node::null();
97
    }
98
623
    if (conflict)
99
    {
100
830
      Trace("strings-eager-pconf")
101
415
          << "Conflict for " << prevC << ", " << c << std::endl;
102
830
      std::vector<Node> ccs;
103
830
      Node r[2];
104
1245
      for (unsigned i = 0; i < 2; i++)
105
      {
106
1660
        Node tp = i == 0 ? t : prev;
107
830
        if (tp.getKind() == STRING_IN_REGEXP)
108
        {
109
268
          ccs.push_back(tp);
110
268
          r[i] = tp[0];
111
        }
112
        else
113
        {
114
562
          r[i] = tp;
115
        }
116
      }
117
415
      if (r[0] != r[1])
118
      {
119
415
        ccs.push_back(r[0].eqNode(r[1]));
120
      }
121
415
      Assert(!ccs.empty());
122
      Node ret =
123
830
          ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
124
830
      Trace("strings-eager-pconf")
125
415
          << "String: eager prefix conflict: " << ret << std::endl;
126
415
      return ret;
127
    }
128
  }
129
6522
  if (isSuf)
130
  {
131
3391
    d_suffixC = t;
132
  }
133
  else
134
  {
135
3131
    d_prefixC = t;
136
  }
137
6522
  return Node::null();
138
}
139
140
}  // namespace strings
141
}  // namespace theory
142
26676
}  // namespace CVC4