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