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