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