GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/example_infer.cpp Lines: 103 123 83.7 %
Date: 2021-03-23 Branches: 165 464 35.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file example_infer.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 Implementation of utility for inferring whether a formula is in
13
 ** examples form (functions applied to concrete arguments only).
14
 **
15
 **/
16
#include "theory/quantifiers/sygus/example_infer.h"
17
18
#include "theory/quantifiers/quant_util.h"
19
20
using namespace CVC4;
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
2190
ExampleInfer::ExampleInfer(TermDbSygus* tds) : d_tds(tds)
28
{
29
2190
  d_isExamples = false;
30
2190
}
31
32
2188
ExampleInfer::~ExampleInfer() {}
33
34
506
bool ExampleInfer::initialize(Node n, const std::vector<Node>& candidates)
35
{
36
506
  Trace("ex-infer") << "Initialize example inference : " << n << std::endl;
37
38
1289
  for (const Node& v : candidates)
39
  {
40
783
    d_examples[v].clear();
41
783
    d_examplesOut[v].clear();
42
783
    d_examplesTerm[v].clear();
43
  }
44
  std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>
45
1012
      visited;
46
  // n is negated conjecture
47
506
  if (!collectExamples(n, visited, true, false))
48
  {
49
3
    Trace("ex-infer") << "...conflicting examples" << std::endl;
50
3
    return false;
51
  }
52
53
503
  if (Trace.isOn("ex-infer"))
54
  {
55
    for (unsigned i = 0; i < candidates.size(); i++)
56
    {
57
      Node v = candidates[i];
58
      Trace("ex-infer") << "  examples for " << v << " : ";
59
      if (d_examples_invalid.find(v) != d_examples_invalid.end())
60
      {
61
        Trace("ex-infer") << "INVALID" << std::endl;
62
      }
63
      else
64
      {
65
        Trace("ex-infer") << std::endl;
66
        for (unsigned j = 0; j < d_examples[v].size(); j++)
67
        {
68
          Trace("ex-infer") << "    ";
69
          for (unsigned k = 0; k < d_examples[v][j].size(); k++)
70
          {
71
            Trace("ex-infer") << d_examples[v][j][k] << " ";
72
          }
73
          if (!d_examplesOut[v][j].isNull())
74
          {
75
            Trace("ex-infer") << " -> " << d_examplesOut[v][j];
76
          }
77
          Trace("ex-infer") << std::endl;
78
        }
79
      }
80
      Trace("ex-infer") << "Initialize " << d_examples[v].size()
81
                        << " example points for " << v << "..." << std::endl;
82
    }
83
  }
84
503
  return true;
85
}
86
87
30712
bool ExampleInfer::collectExamples(
88
    Node n,
89
    std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>&
90
        visited,
91
    bool hasPol,
92
    bool pol)
93
{
94
30712
  std::pair<bool, bool> cacheIndex = std::pair<bool, bool>(hasPol, pol);
95
30712
  if (visited[cacheIndex].find(n) != visited[cacheIndex].end())
96
  {
97
    // already visited
98
13836
    return true;
99
  }
100
16876
  visited[cacheIndex].insert(n);
101
16876
  NodeManager* nm = NodeManager::currentNM();
102
33752
  Node neval;
103
33752
  Node n_output;
104
16876
  bool neval_is_evalapp = false;
105
16876
  if (n.getKind() == DT_SYGUS_EVAL)
106
  {
107
921
    neval = n;
108
921
    if (hasPol)
109
    {
110
80
      n_output = nm->mkConst(pol);
111
    }
112
921
    neval_is_evalapp = true;
113
  }
114
15955
  else if (n.getKind() == EQUAL && hasPol && pol)
115
  {
116
1168
    for (unsigned r = 0; r < 2; r++)
117
    {
118
1124
      if (n[r].getKind() == DT_SYGUS_EVAL)
119
      {
120
742
        neval = n[r];
121
742
        if (n[1 - r].isConst())
122
        {
123
720
          n_output = n[1 - r];
124
        }
125
742
        neval_is_evalapp = true;
126
742
        break;
127
      }
128
    }
129
  }
130
  // is it an evaluation function?
131
16876
  if (neval_is_evalapp && d_examples.find(neval[0]) != d_examples.end())
132
  {
133
3326
    Trace("ex-infer-debug")
134
1663
        << "Process head: " << n << " == " << n_output << std::endl;
135
    // If n_output is null, then neval does not have a constant value
136
    // If n_output is non-null, then neval is constrained to always be
137
    // that value.
138
1663
    if (!n_output.isNull())
139
    {
140
800
      std::map<Node, Node>::iterator itet = d_exampleTermMap.find(neval);
141
800
      if (itet == d_exampleTermMap.end())
142
      {
143
797
        d_exampleTermMap[neval] = n_output;
144
      }
145
3
      else if (itet->second != n_output)
146
      {
147
        // We have a conflicting pair f( c ) = d1 ^ f( c ) = d2 for d1 != d2,
148
        // the conjecture is infeasible.
149
3
        return false;
150
      }
151
    }
152
    // get the evaluation head
153
2537
    Node eh = neval[0];
154
1660
    std::map<Node, bool>::iterator itx = d_examples_invalid.find(eh);
155
1660
    if (itx == d_examples_invalid.end())
156
    {
157
      // have we already processed this as an example term?
158
4314
      if (std::find(d_examplesTerm[eh].begin(), d_examplesTerm[eh].end(), neval)
159
4314
          == d_examplesTerm[eh].end())
160
      {
161
        // collect example
162
1412
        bool success = true;
163
2041
        std::vector<Node> ex;
164
2895
        for (unsigned j = 1, nchild = neval.getNumChildren(); j < nchild; j++)
165
        {
166
1946
          if (!neval[j].isConst())
167
          {
168
463
            success = false;
169
463
            break;
170
          }
171
1483
          ex.push_back(neval[j]);
172
        }
173
1412
        if (success)
174
        {
175
949
          d_examples[eh].push_back(ex);
176
949
          d_examplesOut[eh].push_back(n_output);
177
949
          d_examplesTerm[eh].push_back(neval);
178
949
          if (n_output.isNull())
179
          {
180
166
            d_examplesOut_invalid[eh] = true;
181
          }
182
          else
183
          {
184
783
            Assert(n_output.isConst());
185
            // finished processing this node if it was an I/O pair
186
783
            return true;
187
          }
188
        }
189
        else
190
        {
191
463
          d_examples_invalid[eh] = true;
192
463
          d_examplesOut_invalid[eh] = true;
193
        }
194
      }
195
    }
196
  }
197
46290
  for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
198
  {
199
    bool newHasPol;
200
    bool newPol;
201
30206
    QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol);
202
30206
    if (!collectExamples(n[i], visited, newHasPol, newPol))
203
    {
204
6
      return false;
205
    }
206
  }
207
16084
  return true;
208
}
209
210
883
bool ExampleInfer::hasExamples(Node f) const
211
{
212
883
  std::map<Node, bool>::const_iterator itx = d_examples_invalid.find(f);
213
883
  if (itx == d_examples_invalid.end())
214
  {
215
664
    return d_examples.find(f) != d_examples.end();
216
  }
217
219
  return false;
218
}
219
220
874
unsigned ExampleInfer::getNumExamples(Node f) const
221
{
222
  std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
223
874
      d_examples.find(f);
224
874
  if (it != d_examples.end())
225
  {
226
874
    return it->second.size();
227
  }
228
  return 0;
229
}
230
231
1664
void ExampleInfer::getExample(Node f, unsigned i, std::vector<Node>& ex) const
232
{
233
1664
  Assert(!f.isNull());
234
  std::map<Node, std::vector<std::vector<Node>>>::const_iterator it =
235
1664
      d_examples.find(f);
236
1664
  if (it != d_examples.end())
237
  {
238
1664
    Assert(i < it->second.size());
239
1664
    ex.insert(ex.end(), it->second[i].begin(), it->second[i].end());
240
  }
241
  else
242
  {
243
    Assert(false);
244
  }
245
1664
}
246
247
3398
void ExampleInfer::getExampleTerms(Node f, std::vector<Node>& exTerms) const
248
{
249
  std::map<Node, std::vector<Node>>::const_iterator itt =
250
3398
      d_examplesTerm.find(f);
251
3398
  if (itt == d_examplesTerm.end())
252
  {
253
    return;
254
  }
255
3398
  exTerms.insert(exTerms.end(), itt->second.begin(), itt->second.end());
256
}
257
258
675
Node ExampleInfer::getExampleOut(Node f, unsigned i) const
259
{
260
675
  Assert(!f.isNull());
261
675
  std::map<Node, std::vector<Node>>::const_iterator it = d_examplesOut.find(f);
262
675
  if (it != d_examplesOut.end())
263
  {
264
675
    Assert(i < it->second.size());
265
675
    return it->second[i];
266
  }
267
  Assert(false);
268
  return Node::null();
269
}
270
271
140
bool ExampleInfer::hasExamplesOut(Node f) const
272
{
273
140
  return d_examplesOut_invalid.find(f) == d_examplesOut_invalid.end();
274
}
275
276
}  // namespace quantifiers
277
}  // namespace theory
278
26685
}  // namespace CVC4