src/theory/quantifiers/expr_miner.h

   1 /*********************                                                        */
   2 /*! \file expr_miner.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-2020 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 expr_miner
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
  18 #define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
  19
  20 #include <map>
  21 #include <memory>
  22 #include <vector>
  23
  24 #include "expr/expr.h"
  25 #include "expr/expr_manager.h"
  26 #include "expr/variable_type_map.h"
  27 #include "smt/smt_engine.h"
  28 #include "theory/quantifiers/sygus_sampler.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32 namespace quantifiers {
  33
  34 /** Expression miner
  35  *
  36  * This is a virtual base class for modules that "mines" certain information
  37  * from (enumerated) expressions. This includes:
  38  * - candidate rewrite rules (--sygus-rr-synth)
  39  */
  40 class ExprMiner
  41 {
  42  public:
  43   ExprMiner() : d_sampler(nullptr) {}
  44   virtual ~ExprMiner() {}
  45   /** initialize
  46    *
  47    * This initializes this expression miner. The argument vars indicates the
  48    * free variables of terms that will be added to this class. The argument
  49    * sampler gives an (optional) pointer to a sampler, which is used to
  50    * sample tuples of valuations of these variables.
  51    */
  52   virtual void initialize(const std::vector<Node>& vars,
  53                           SygusSampler* ss = nullptr);
  54   /** add term
  55    *
  56    * This registers term n with this expression miner. The output stream out
  57    * is provided as an argument for the purposes of outputting the result of
  58    * the expression mining done by this class. For example, candidate-rewrite
  59    * output is printed on out by the candidate rewrite generator miner.
  60    */
  61   virtual bool addTerm(Node n, std::ostream& out) = 0;
  62
  63  protected:
  64   /** the set of variables used by this class */
  65   std::vector<Node> d_vars;
  66   /** pointer to the sygus sampler object we are using */
  67   SygusSampler* d_sampler;
  68   /**
  69    * Maps to skolems for each free variable that appears in a check. This is
  70    * used during initializeChecker so that query (which may contain free
  71    * variables) is converted to a formula without free variables.
  72    */
  73   std::map<Node, Node> d_fv_to_skolem;
  74   /** convert */
  75   Node convertToSkolem(Node n);
  76   /** initialize checker
  77    *
  78    * This function initializes the smt engine smte to check the satisfiability
  79    * of the argument "query", which is a formula whose free variables (of
  80    * kind BOUND_VARIABLE) are a subset of d_vars.
  81    *
  82    * The arguments em and varMap are used for supporting cases where we
  83    * want smte to use a different expression manager instead of the current
  84    * expression manager. The motivation for this so that different options can
  85    * be set for the subcall.
  86    *
  87    * We update the flag needExport to true if smte is using the expression
  88    * manager em. In this case, subsequent expressions extracted from smte
  89    * (for instance, model values) must be exported to the current expression
  90    * manager.
  91    */
  92   void initializeChecker(std::unique_ptr<SmtEngine>& smte,
  93                          ExprManager& em,
  94                          ExprManagerMapCollection& varMap,
  95                          Node query,
  96                          bool& needExport);
  97   /**
  98    * Run the satisfiability check on query and return the result
  99    * (sat/unsat/unknown).
 100    *
 101    * In contrast to the above method, this call should be used for cases where
 102    * the model for the query is not important.
 103    */
 104   Result doCheck(Node query);
 105 };
 106
 107 }  // namespace quantifiers
 108 }  // namespace theory
 109 }  // namespace CVC4
 110
 111 #endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */