src/theory/quantifiers/query_generator.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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  * ****************************************************************************
  12  *
  13  * A class for mining interesting satisfiability queries from a stream
  14  * of generated expressions.
  15  */
  16
  17 #include "cvc5_private.h"
  18
  19 #ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
  20 #define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
  21
  22 #include <map>
  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"
  28
  29 namespace cvc5 {
  30 namespace theory {
  31 namespace quantifiers {
  32
  33 /** QueryGenerator
  34  *
  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.
  39  *
  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.
  46  *
  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
  50  * query as well.
  51  */
  52 class QueryGenerator : public ExprMiner
  53 {
  54  public:
  55   QueryGenerator(Env& env);
  56   ~QueryGenerator() {}
  57   /** initialize */
  58   void initialize(const std::vector<Node>& vars,
  59                   SygusSampler* ss = nullptr) override;
  60   /**
  61    * Add term to this module. This may trigger the printing and/or checking of
  62    * new queries.
  63    */
  64   bool addTerm(Node n, std::ostream& out) override;
  65   /**
  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.
  68    */
  69   void setThreshold(unsigned deqThresh);
  70
  71  private:
  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 */
  75   unsigned d_deqThresh;
  76   /**
  77    * For each type, a lazy trie storing the evaluation of all added terms on
  78    * sample points.
  79    */
  80   std::map<TypeNode, LazyTrie> d_qgtTrie;
  81   /** total number of queries generated by this class */
  82   unsigned d_queryCount;
  83   /** find queries
  84    *
  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
  90    * class).
  91    */
  92   void findQueries(Node n,
  93                    std::vector<Node>& queries,
  94                    std::vector<std::vector<unsigned>>& queriesPtTrue);
  95   /**
  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.
  99    */
 100   std::map<unsigned, std::vector<Node>> d_ptToQueries;
 101   /**
 102    * Map from queries to the indices of the points that satisfy them.
 103    */
 104   std::map<Node, std::vector<unsigned>> d_qysToPoints;
 105   /**
 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.
 109    */
 110   void checkQuery(Node qy, unsigned spIndex);
 111   /**
 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).
 114    */
 115   void dumpQuery(Node qy, unsigned spIndex);
 116 };
 117
 118 }  // namespace quantifiers
 119 }  // namespace theory
 120 }  // namespace cvc5
 121
 122 #endif /* CVC5__THEORY__QUANTIFIERS___H */