GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/dynamic_rewrite.cpp Lines: 74 87 85.1 %
Date: 2021-03-23 Branches: 163 360 45.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dynamic_rewrite.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 dynamic_rewriter
13
 **/
14
15
#include "theory/quantifiers/dynamic_rewrite.h"
16
17
#include "theory/rewriter.h"
18
19
using namespace std;
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
26
8
DynamicRewriter::DynamicRewriter(const std::string& name,
27
8
                                 context::UserContext* u)
28
8
    : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
29
{
30
8
  d_equalityEngine.addFunctionKind(kind::APPLY_UF);
31
8
}
32
33
149
void DynamicRewriter::addRewrite(Node a, Node b)
34
{
35
149
  Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
36
149
  if (a == b)
37
  {
38
    Trace("dyn-rewrite") << "...equal." << std::endl;
39
    return;
40
  }
41
42
  // add to the equality engine
43
298
  Node ai = toInternal(a);
44
298
  Node bi = toInternal(b);
45
149
  if (ai.isNull() || bi.isNull())
46
  {
47
    Trace("dyn-rewrite") << "...not internalizable." << std::endl;
48
    return;
49
  }
50
149
  Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
51
52
149
  Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
53
298
  Node eq = ai.eqNode(bi);
54
149
  d_rewrites.push_back(eq);
55
149
  d_equalityEngine.assertEquality(eq, true, eq);
56
149
  Assert(d_equalityEngine.consistent());
57
149
  Trace("dyn-rewrite-debug") << "Finished" << std::endl;
58
}
59
60
1179
bool DynamicRewriter::areEqual(Node a, Node b)
61
{
62
1179
  if (a == b)
63
  {
64
    return true;
65
  }
66
1179
  Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl;
67
  // add to the equality engine
68
2358
  Node ai = toInternal(a);
69
2358
  Node bi = toInternal(b);
70
1179
  if (ai.isNull() || bi.isNull())
71
  {
72
    Trace("dyn-rewrite") << "...not internalizable." << std::endl;
73
    return false;
74
  }
75
1179
  Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl;
76
1179
  d_equalityEngine.addTerm(ai);
77
1179
  d_equalityEngine.addTerm(bi);
78
1179
  Trace("dyn-rewrite-debug") << "...added terms" << std::endl;
79
1179
  return d_equalityEngine.areEqual(ai, bi);
80
}
81
82
5847
Node DynamicRewriter::toInternal(Node a)
83
{
84
5847
  std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
85
5847
  if (it != d_term_to_internal.end())
86
  {
87
4410
    return it->second;
88
  }
89
2874
  Node ret = a;
90
91
1437
  if (!a.isVar())
92
  {
93
2852
    std::vector<Node> children;
94
1426
    if (a.hasOperator())
95
    {
96
2830
      Node op = a.getOperator();
97
1415
      if (a.getKind() != APPLY_UF)
98
      {
99
1415
        op = d_ois_trie[op].getSymbol(a);
100
        // if this term involves an argument that is not of first class type,
101
        // we cannot reason about it. This includes operators like str.in-re.
102
1415
        if (op.isNull())
103
        {
104
          return Node::null();
105
        }
106
      }
107
1415
      children.push_back(op);
108
    }
109
4244
    for (const Node& ca : a)
110
    {
111
5636
      Node cai = toInternal(ca);
112
2818
      if (cai.isNull())
113
      {
114
        return Node::null();
115
      }
116
2818
      children.push_back(cai);
117
    }
118
1426
    if (!children.empty())
119
    {
120
1415
      if (children.size() == 1)
121
      {
122
        ret = children[0];
123
      }
124
      else
125
      {
126
1415
        ret = NodeManager::currentNM()->mkNode(APPLY_UF, children);
127
      }
128
    }
129
  }
130
1437
  d_term_to_internal[a] = ret;
131
1437
  d_internal_to_term[ret] = a;
132
1437
  return ret;
133
}
134
135
366
Node DynamicRewriter::toExternal(Node ai)
136
{
137
366
  std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
138
366
  if (it != d_internal_to_term.end())
139
  {
140
366
    return it->second;
141
  }
142
  return Node::null();
143
}
144
145
1415
Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
146
{
147
2830
  std::vector<TypeNode> ctypes;
148
4233
  for (const Node& cn : n)
149
  {
150
2818
    ctypes.push_back(cn.getType());
151
  }
152
1415
  ctypes.push_back(n.getType());
153
154
1415
  OpInternalSymTrie* curr = this;
155
5648
  for (unsigned i = 0, size = ctypes.size(); i < size; i++)
156
  {
157
    // cannot handle certain types (e.g. regular expressions or functions)
158
4233
    if (!ctypes[i].isFirstClass())
159
    {
160
      return Node::null();
161
    }
162
4233
    curr = &(curr->d_children[ctypes[i]]);
163
  }
164
1415
  if (!curr->d_sym.isNull())
165
  {
166
1380
    return curr->d_sym;
167
  }
168
  // make UF operator
169
70
  TypeNode utype;
170
35
  if (ctypes.size() == 1)
171
  {
172
    utype = ctypes[0];
173
  }
174
  else
175
  {
176
35
    utype = NodeManager::currentNM()->mkFunctionType(ctypes);
177
  }
178
  Node f = NodeManager::currentNM()->mkSkolem(
179
70
      "ufd", utype, "internal op for dynamic_rewriter");
180
35
  curr->d_sym = f;
181
35
  return f;
182
}
183
184
} /* CVC4::theory::quantifiers namespace */
185
} /* CVC4::theory namespace */
186
26685
} /* CVC4 namespace */