GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/query_generator.cpp Lines: 2 223 0.9 %
Date: 2021-03-23 Branches: 2 684 0.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file query_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
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 a class for mining interesting satisfiability
13
 ** queries from a stream of generated expressions.
14
 **/
15
16
#include "theory/quantifiers/query_generator.h"
17
18
#include <fstream>
19
20
#include "api/cvc4cpp.h"
21
#include "options/quantifiers_options.h"
22
#include "smt/smt_engine.h"
23
#include "smt/smt_engine_scope.h"
24
#include "util/random.h"
25
26
using namespace std;
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
12
QueryGenerator::QueryGenerator() : d_queryCount(0) {}
34
void QueryGenerator::initialize(const std::vector<Node>& vars, SygusSampler* ss)
35
{
36
  Assert(ss != nullptr);
37
  d_queryCount = 0;
38
  ExprMiner::initialize(vars, ss);
39
}
40
41
void QueryGenerator::setThreshold(unsigned deqThresh)
42
{
43
  d_deqThresh = deqThresh;
44
}
45
46
bool QueryGenerator::addTerm(Node n, std::ostream& out)
47
{
48
  Node nn = n.getKind() == NOT ? n[0] : n;
49
  if (d_terms.find(nn) != d_terms.end())
50
  {
51
    return false;
52
  }
53
  d_terms.insert(nn);
54
55
  Trace("sygus-qgen") << "QueryGenerator::addTerm : " << n << std::endl;
56
  unsigned npts = d_sampler->getNumSamplePoints();
57
  TypeNode tn = n.getType();
58
  // TODO : as an optimization, use a shared lazy trie?
59
60
  // the queries we generate on this round
61
  std::vector<Node> queries;
62
  // For each query in the above vector, this stores the indices of the points
63
  // for which that query evaluated to true on.
64
  std::vector<std::vector<unsigned>> queriesPtTrue;
65
  // the sample point indices for which the above queries are true
66
  std::unordered_set<unsigned> indices;
67
68
  // collect predicate queries (if n is Boolean)
69
  if (tn.isBoolean())
70
  {
71
    std::map<Node, std::vector<unsigned>> ev_to_pt;
72
    unsigned index = 0;
73
    unsigned threshCount = 0;
74
    while (index < npts && threshCount < 2)
75
    {
76
      Node v = d_sampler->evaluate(nn, index);
77
      ev_to_pt[v].push_back(index);
78
      if (ev_to_pt[v].size() == d_deqThresh + 1)
79
      {
80
        threshCount++;
81
      }
82
      index++;
83
    }
84
    if (threshCount < 2)
85
    {
86
      for (const auto& etp : ev_to_pt)
87
      {
88
        if (etp.second.size() < d_deqThresh)
89
        {
90
          indices.insert(etp.second.begin(), etp.second.end());
91
          Node qy = nn;
92
          Assert(etp.first.isConst());
93
          if (!etp.first.getConst<bool>())
94
          {
95
            qy = qy.negate();
96
          }
97
          queries.push_back(qy);
98
          queriesPtTrue.push_back(etp.second);
99
        }
100
      }
101
    }
102
  }
103
104
  // collect equality queries
105
  findQueries(nn, queries, queriesPtTrue);
106
  Assert(queries.size() == queriesPtTrue.size());
107
  if (queries.empty())
108
  {
109
    return true;
110
  }
111
  Trace("sygus-qgen-debug")
112
      << "query: Check " << queries.size() << " queries..." << std::endl;
113
  // literal queries
114
  for (unsigned i = 0, nqueries = queries.size(); i < nqueries; i++)
115
  {
116
    Node qy = queries[i];
117
    std::vector<unsigned>& tIndices = queriesPtTrue[i];
118
    // we have an interesting query
119
    out << "(query " << qy << ")  ; " << tIndices.size() << "/" << npts
120
        << std::endl;
121
    AlwaysAssert(!tIndices.empty());
122
    checkQuery(qy, tIndices[0]);
123
    // add information
124
    for (unsigned& ti : tIndices)
125
    {
126
      d_ptToQueries[ti].push_back(qy);
127
      d_qysToPoints[qy].push_back(ti);
128
      indices.insert(ti);
129
    }
130
  }
131
  // for each new index, we may have a new conjunctive query
132
  NodeManager* nm = NodeManager::currentNM();
133
  for (const unsigned& i : indices)
134
  {
135
    std::vector<Node>& qsi = d_ptToQueries[i];
136
    if (qsi.size() > 1)
137
    {
138
      // take two random queries
139
      std::shuffle(qsi.begin(), qsi.end(), Random::getRandom());
140
      Node qy = nm->mkNode(AND, qsi[0], qsi[1]);
141
      checkQuery(qy, i);
142
    }
143
  }
144
  Trace("sygus-qgen-check") << "...finished." << std::endl;
145
  return true;
146
}
147
148
void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
149
{
150
  // external query
151
  if (options::sygusQueryGenDumpFiles()
152
      == options::SygusQueryDumpFilesMode::ALL)
153
  {
154
    dumpQuery(qy, spIndex);
155
  }
156
157
  if (options::sygusQueryGenCheck())
158
  {
159
    Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
160
    // make the satisfiability query
161
    std::unique_ptr<SmtEngine> queryChecker;
162
    initializeChecker(queryChecker, qy);
163
    Result r = queryChecker->checkSat();
164
    Trace("sygus-qgen-check") << "  query: ...got : " << r << std::endl;
165
    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
166
    {
167
      std::stringstream ss;
168
      ss << "--sygus-rr-query-gen detected unsoundness in CVC4 on input " << qy
169
         << "!" << std::endl;
170
      ss << "This query has a model : " << std::endl;
171
      std::vector<Node> pt;
172
      d_sampler->getSamplePoint(spIndex, pt);
173
      Assert(pt.size() == d_vars.size());
174
      for (unsigned i = 0, size = pt.size(); i < size; i++)
175
      {
176
        ss << "  " << d_vars[i] << " -> " << pt[i] << std::endl;
177
      }
178
      ss << "but CVC4 answered unsat!" << std::endl;
179
      AlwaysAssert(false) << ss.str();
180
    }
181
    if (options::sygusQueryGenDumpFiles()
182
        == options::SygusQueryDumpFilesMode::UNSOLVED)
183
    {
184
      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
185
      {
186
        dumpQuery(qy, spIndex);
187
      }
188
    }
189
  }
190
191
  d_queryCount++;
192
}
193
194
void QueryGenerator::dumpQuery(Node qy, unsigned spIndex)
195
{
196
  // Print the query and the query + its model (commented) to queryN.smt2
197
  std::vector<Node> pt;
198
  d_sampler->getSamplePoint(spIndex, pt);
199
  size_t nvars = d_vars.size();
200
  AlwaysAssert(pt.size() == d_vars.size());
201
  std::stringstream fname;
202
  fname << "query" << d_queryCount << ".smt2";
203
  std::ofstream fs(fname.str(), std::ofstream::out);
204
  fs << "(set-logic ALL)" << std::endl;
205
  for (unsigned i = 0; i < 2; i++)
206
  {
207
    for (size_t j = 0; j < nvars; j++)
208
    {
209
      Node x = d_vars[j];
210
      if (i == 0)
211
      {
212
        fs << "(declare-fun " << x << " () " << x.getType() << ")";
213
      }
214
      else
215
      {
216
        fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j]
217
           << ")";
218
      }
219
      fs << std::endl;
220
    }
221
  }
222
  fs << "(assert " << qy << ")" << std::endl;
223
  fs << "(check-sat)" << std::endl;
224
  fs.close();
225
}
226
227
void QueryGenerator::findQueries(
228
    Node n,
229
    std::vector<Node>& queries,
230
    std::vector<std::vector<unsigned>>& queriesPtTrue)
231
{
232
  // At a high level, this method traverses the LazyTrie for the type of n
233
  // and tries to find paths to leafs that contain terms n' such that n = n'
234
  // or n != n' is an interesting query, i.e. satisfied for a small number of
235
  // points.
236
  TypeNode tn = n.getType();
237
  LazyTrie* lt = &d_qgtTrie[tn];
238
  // These vectors are the set of indices of sample points for which the current
239
  // node we are considering are { equal, disequal } from n.
240
  std::vector<unsigned> eqIndex[2];
241
  Trace("sygus-qgen-debug") << "Compute queries for " << n << "...\n";
242
243
  LazyTrieEvaluator* ev = d_sampler;
244
  unsigned ntotal = d_sampler->getNumSamplePoints();
245
  unsigned index = 0;
246
  bool exact = true;
247
  bool pushEq[2] = {false, false};
248
  bool pre = true;
249
  // The following parallel vectors describe the state of the locations in the
250
  // trie we are currently visiting.
251
  // Reference to the location in the trie
252
  std::vector<LazyTrie*> visitTr;
253
  // The index of the sample point we are testing
254
  std::vector<unsigned> currIndex;
255
  // Whether the path to this location exactly matches the evaluation of n
256
  std::vector<bool> currExact;
257
  // Whether we are adding to the points that are { equal, disequal } by
258
  // traversing to this location.
259
  std::vector<bool> pushIndex[2];
260
  // Whether we are in a pre-traversal for this location.
261
  std::vector<bool> preVisit;
262
  visitTr.push_back(lt);
263
  currIndex.push_back(0);
264
  currExact.push_back(true);
265
  pushIndex[0].push_back(false);
266
  pushIndex[1].push_back(false);
267
  preVisit.push_back(true);
268
  do
269
  {
270
    lt = visitTr.back();
271
    index = currIndex.back();
272
    exact = currExact.back();
273
    for (unsigned r = 0; r < 2; r++)
274
    {
275
      pushEq[r] = pushIndex[r].back();
276
    }
277
    pre = preVisit.back();
278
    if (!pre)
279
    {
280
      visitTr.pop_back();
281
      currIndex.pop_back();
282
      currExact.pop_back();
283
      preVisit.pop_back();
284
      // clean up the indices of points that are { equal, disequal }
285
      for (unsigned r = 0; r < 2; r++)
286
      {
287
        if (pushEq[r])
288
        {
289
          eqIndex[r].pop_back();
290
        }
291
        pushIndex[r].pop_back();
292
      }
293
    }
294
    else
295
    {
296
      preVisit[preVisit.size() - 1] = false;
297
      // add to the indices of points that are { equal, disequal }
298
      for (unsigned r = 0; r < 2; r++)
299
      {
300
        if (pushEq[r])
301
        {
302
          eqIndex[r].push_back(index - 1);
303
        }
304
      }
305
      int eqAllow = d_deqThresh - eqIndex[0].size();
306
      int deqAllow = d_deqThresh - eqIndex[1].size();
307
      Trace("sygus-qgen-debug")
308
          << "Find queries " << n << " " << index << "/" << ntotal
309
          << ", deq/eq allow = " << deqAllow << "/" << eqAllow
310
          << ", exact = " << exact << std::endl;
311
      if (index == ntotal)
312
      {
313
        if (exact)
314
        {
315
          // add to the trie
316
          lt->d_lazy_child = n;
317
        }
318
        else
319
        {
320
          Node nAlmostEq = lt->d_lazy_child;
321
          // if made it here, we still should have either a equality or
322
          // a disequality that is allowed.
323
          Assert(deqAllow >= 0 || eqAllow >= 0);
324
          Node query = n.eqNode(nAlmostEq);
325
          std::vector<unsigned> tIndices;
326
          if (eqAllow >= 0)
327
          {
328
            tIndices.insert(
329
                tIndices.end(), eqIndex[0].begin(), eqIndex[0].end());
330
          }
331
          else if (deqAllow >= 0)
332
          {
333
            query = query.negate();
334
            tIndices.insert(
335
                tIndices.end(), eqIndex[1].begin(), eqIndex[1].end());
336
          }
337
          AlwaysAssert(tIndices.size() <= d_deqThresh);
338
          if (!tIndices.empty())
339
          {
340
            queries.push_back(query);
341
            queriesPtTrue.push_back(tIndices);
342
          }
343
        }
344
      }
345
      else
346
      {
347
        if (!lt->d_lazy_child.isNull())
348
        {
349
          // if there is a lazy child here, push
350
          Node e_lc = ev->evaluate(lt->d_lazy_child, index);
351
          // store at next level
352
          lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child;
353
          // replace
354
          lt->d_lazy_child = Node::null();
355
        }
356
        // compute
357
        Node e_this = ev->evaluate(n, index);
358
359
        if (deqAllow >= 0)
360
        {
361
          // recursing on disequal points
362
          deqAllow--;
363
          // if there is use continuing
364
          if (deqAllow >= 0 || eqAllow >= 0)
365
          {
366
            for (std::pair<const Node, LazyTrie>& ltc : lt->d_children)
367
            {
368
              if (ltc.first != e_this)
369
              {
370
                visitTr.push_back(&ltc.second);
371
                currIndex.push_back(index + 1);
372
                currExact.push_back(false);
373
                pushIndex[0].push_back(false);
374
                pushIndex[1].push_back(true);
375
                preVisit.push_back(true);
376
              }
377
            }
378
          }
379
          deqAllow++;
380
        }
381
        bool pushEqNext = false;
382
        if (eqAllow >= 0)
383
        {
384
          // below, we try recursing (if at all) on equal nodes.
385
          eqAllow--;
386
          pushEqNext = true;
387
        }
388
        // if we are on the exact path of n
389
        if (exact)
390
        {
391
          if (lt->d_children.empty())
392
          {
393
            // if no one has been here before, we are done
394
            lt->d_lazy_child = n;
395
          }
396
          else
397
          {
398
            // otherwise, we recurse on the equal point
399
            visitTr.push_back(&(lt->d_children[e_this]));
400
            currIndex.push_back(index + 1);
401
            currExact.push_back(true);
402
            pushIndex[0].push_back(pushEqNext);
403
            pushIndex[1].push_back(false);
404
            preVisit.push_back(true);
405
          }
406
        }
407
        else if (deqAllow >= 0 || eqAllow >= 0)
408
        {
409
          // recurse on the equal point if it exists
410
          std::map<Node, LazyTrie>::iterator iteq = lt->d_children.find(e_this);
411
          if (iteq != lt->d_children.end())
412
          {
413
            visitTr.push_back(&(iteq->second));
414
            currIndex.push_back(index + 1);
415
            currExact.push_back(false);
416
            pushIndex[0].push_back(pushEqNext);
417
            pushIndex[1].push_back(false);
418
            preVisit.push_back(true);
419
          }
420
        }
421
      }
422
    }
423
  } while (!visitTr.empty());
424
}
425
426
}  // namespace quantifiers
427
}  // namespace theory
428
26685
}  // namespace CVC4