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