GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_registry.cpp Lines: 74 95 77.9 %
Date: 2021-03-22 Branches: 84 228 36.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_registry.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters
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 quantifiers registry
13
 **/
14
15
#include "theory/quantifiers/quantifiers_registry.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/quant_module.h"
19
#include "theory/quantifiers/term_util.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
8995
QuantifiersRegistry::QuantifiersRegistry()
26
    : d_quantAttr(),
27
17990
      d_quantBoundInf(options::fmfTypeCompletionThresh(),
28
17990
                      options::finiteModelFind())
29
{
30
8995
}
31
32
48743
void QuantifiersRegistry::registerQuantifier(Node q)
33
{
34
48743
  if (d_inst_constants.find(q) != d_inst_constants.end())
35
  {
36
25256
    return;
37
  }
38
23487
  NodeManager* nm = NodeManager::currentNM();
39
46974
  Debug("quantifiers-engine")
40
23487
      << "Instantiation constants for " << q << " : " << std::endl;
41
77929
  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
42
  {
43
54442
    d_vars[q].push_back(q[0][i]);
44
    // make instantiation constants
45
108884
    Node ic = nm->mkInstConstant(q[0][i].getType());
46
54442
    d_inst_constants_map[ic] = q;
47
54442
    d_inst_constants[q].push_back(ic);
48
54442
    Debug("quantifiers-engine") << "  " << ic << std::endl;
49
    // set the var number attribute
50
    InstVarNumAttribute ivna;
51
54442
    ic.setAttribute(ivna, i);
52
    InstConstantAttribute ica;
53
54442
    ic.setAttribute(ica, q);
54
  }
55
  // compute attributes
56
23487
  d_quantAttr.computeAttributes(q);
57
}
58
59
28251
bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
60
61
28251
std::string QuantifiersRegistry::identify() const
62
{
63
28251
  return "QuantifiersRegistry";
64
}
65
66
456291
QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
67
{
68
456291
  std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
69
456291
  if (it == d_owner.end())
70
  {
71
424585
    return nullptr;
72
  }
73
31706
  return it->second;
74
}
75
76
2322
void QuantifiersRegistry::setOwner(Node q,
77
                                   QuantifiersModule* m,
78
                                   int32_t priority)
79
{
80
2322
  QuantifiersModule* mo = getOwner(q);
81
2322
  if (mo == m)
82
  {
83
    return;
84
  }
85
2322
  if (mo != nullptr)
86
  {
87
    if (priority <= d_owner_priority[q])
88
    {
89
      Trace("quant-warn") << "WARNING: setting owner of " << q << " to "
90
                          << (m ? m->identify() : "null")
91
                          << ", but already has owner " << mo->identify()
92
                          << " with higher priority!" << std::endl;
93
      return;
94
    }
95
  }
96
2322
  d_owner[q] = m;
97
2322
  d_owner_priority[q] = priority;
98
}
99
100
401753
bool QuantifiersRegistry::hasOwnership(Node q, QuantifiersModule* m) const
101
{
102
401753
  QuantifiersModule* mo = getOwner(q);
103
401753
  return mo == m || mo == nullptr;
104
}
105
106
58297
Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
107
{
108
  std::map<Node, std::vector<Node> >::const_iterator it =
109
58297
      d_inst_constants.find(q);
110
58297
  if (it != d_inst_constants.end())
111
  {
112
58297
    return it->second[i];
113
  }
114
  return Node::null();
115
}
116
117
25213
size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
118
{
119
  std::map<Node, std::vector<Node> >::const_iterator it =
120
25213
      d_inst_constants.find(q);
121
25213
  if (it != d_inst_constants.end())
122
  {
123
25213
    return it->second.size();
124
  }
125
  return 0;
126
}
127
128
128028
Node QuantifiersRegistry::getInstConstantBody(Node q)
129
{
130
128028
  std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
131
128028
  if (it == d_inst_const_body.end())
132
  {
133
42964
    Node n = substituteBoundVariablesToInstConstants(q[1], q);
134
21482
    d_inst_const_body[q] = n;
135
21482
    return n;
136
  }
137
106546
  return it->second;
138
}
139
140
25246
Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
141
                                                                  Node q)
142
{
143
25246
  registerQuantifier(q);
144
25246
  return n.substitute(d_vars[q].begin(),
145
25246
                      d_vars[q].end(),
146
25246
                      d_inst_constants[q].begin(),
147
100984
                      d_inst_constants[q].end());
148
}
149
150
Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
151
                                                                  Node q)
152
{
153
  registerQuantifier(q);
154
  return n.substitute(d_inst_constants[q].begin(),
155
                      d_inst_constants[q].end(),
156
                      d_vars[q].begin(),
157
                      d_vars[q].end());
158
}
159
160
16
Node QuantifiersRegistry::substituteBoundVariables(Node n,
161
                                                   Node q,
162
                                                   std::vector<Node>& terms)
163
{
164
16
  registerQuantifier(q);
165
16
  Assert(d_vars[q].size() == terms.size());
166
  return n.substitute(
167
16
      d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
168
}
169
170
Node QuantifiersRegistry::substituteInstConstants(Node n,
171
                                                  Node q,
172
                                                  std::vector<Node>& terms)
173
{
174
  registerQuantifier(q);
175
  Assert(d_inst_constants[q].size() == terms.size());
176
  return n.substitute(d_inst_constants[q].begin(),
177
                      d_inst_constants[q].end(),
178
                      terms.begin(),
179
                      terms.end());
180
}
181
182
67755
QuantAttributes& QuantifiersRegistry::getQuantAttributes()
183
{
184
67755
  return d_quantAttr;
185
}
186
187
25144
QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference()
188
{
189
25144
  return d_quantBoundInf;
190
}
191
192
24
Node QuantifiersRegistry::getNameForQuant(Node q) const
193
{
194
48
  Node name = d_quantAttr.getQuantName(q);
195
24
  if (!name.isNull())
196
  {
197
10
    return name;
198
  }
199
14
  return q;
200
}
201
202
24
bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
203
{
204
24
  name = getNameForQuant(q);
205
  // if we have a name, or we did not require one
206
24
  return name != q || !req;
207
}
208
209
}  // namespace quantifiers
210
}  // namespace theory
211
35671
}  // namespace CVC4