GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/query_generator.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file query_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 A class for mining interesting satisfiability queries from a stream
13
 ** of generated expressions.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
19
#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
20
21
#include <map>
22
#include <unordered_set>
23
#include "expr/node.h"
24
#include "theory/quantifiers/expr_miner.h"
25
#include "theory/quantifiers/lazy_trie.h"
26
#include "theory/quantifiers/sygus_sampler.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
/** QueryGenerator
33
 *
34
 * This module is used for finding satisfiable queries that are maximally
35
 * likely to trigger an unsound response in an SMT solver. These queries are
36
 * mined from a stream of enumerated expressions. We judge likelihood of
37
 * triggering unsoundness by the frequency at which the query is satisfied.
38
 *
39
 * In detail, given a stream of expressions t_1, ..., t_{n-1}, upon generating
40
 * term t_n, we consider a query (not) t_n = t_i to be an interesting query
41
 * if it is satisfied by at most D points, where D is a predefined threshold
42
 * given by options::sygusQueryGenThresh(). If t_n has type Bool, we
43
 * additionally consider the case where t_n is satisfied (or not satisfied) by
44
 * fewer than D points.
45
 *
46
 * In addition to generating single literal queries, this module also generates
47
 * conjunctive queries, for instance, by remembering that literals L1 and L2
48
 * were both satisfied by the same point, and thus L1 ^ L2 is an interesting
49
 * query as well.
50
 */
51
class QueryGenerator : public ExprMiner
52
{
53
 public:
54
  QueryGenerator();
55
12
  ~QueryGenerator() {}
56
  /** initialize */
57
  void initialize(const std::vector<Node>& vars,
58
                  SygusSampler* ss = nullptr) override;
59
  /**
60
   * Add term to this module. This may trigger the printing and/or checking of
61
   * new queries.
62
   */
63
  bool addTerm(Node n, std::ostream& out) override;
64
  /**
65
   * Set the threshold value. This is the maximal number of sample points that
66
   * each query we generate is allowed to be satisfied by.
67
   */
68
  void setThreshold(unsigned deqThresh);
69
70
 private:
71
  /** cache of all terms registered to this generator */
72
  std::unordered_set<Node, NodeHashFunction> d_terms;
73
  /** the threshold used by this module for maximum number of sat points */
74
  unsigned d_deqThresh;
75
  /**
76
   * For each type, a lazy trie storing the evaluation of all added terms on
77
   * sample points.
78
   */
79
  std::map<TypeNode, LazyTrie> d_qgtTrie;
80
  /** total number of queries generated by this class */
81
  unsigned d_queryCount;
82
  /** find queries
83
   *
84
   * This function traverses the lazy trie for the type of n, finding equality
85
   * and disequality queries between n and other terms in the trie. The argument
86
   * queries collects the newly generated queries, and the argument
87
   * queriesPtTrue collects the indices of points that each query was satisfied
88
   * by (these indices are the indices of the points in the sampler used by this
89
   * class).
90
   */
91
  void findQueries(Node n,
92
                   std::vector<Node>& queries,
93
                   std::vector<std::vector<unsigned>>& queriesPtTrue);
94
  /**
95
   * Maps the index of each sample point to the list of queries that it
96
   * satisfies, and that were generated by the above function. This map is used
97
   * for generating conjunctive queries.
98
   */
99
  std::map<unsigned, std::vector<Node>> d_ptToQueries;
100
  /**
101
   * Map from queries to the indices of the points that satisfy them.
102
   */
103
  std::map<Node, std::vector<unsigned>> d_qysToPoints;
104
  /**
105
   * Check query qy, which is satisfied by (at least) sample point spIndex,
106
   * using a separate copy of the SMT engine. Throws an exception if qy is
107
   * reported to be unsatisfiable.
108
   */
109
  void checkQuery(Node qy, unsigned spIndex);
110
  /**
111
   * Dumps query qy to the a file queryN.smt2 for the current counter N;
112
   * spIndex specifies the sample point that satisfies it (for debugging).
113
   */
114
  void dumpQuery(Node qy, unsigned spIndex);
115
};
116
117
}  // namespace quantifiers
118
}  // namespace theory
119
}  // namespace CVC4
120
121
#endif /* CVC4__THEORY__QUANTIFIERS___H */