08d7f40b1e5ef48f15bef6393729e8be9eceda4c
1 /********************* */
4 ** Top contributors (to current version):
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
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
18 #define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
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"
32 namespace quantifiers
{
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)
43 ExprMiner() : d_sampler(nullptr) {}
44 virtual ~ExprMiner() {}
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.
52 virtual void initialize(const std::vector
<Node
>& vars
,
53 SygusSampler
* ss
= nullptr);
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.
61 virtual bool addTerm(Node n
, std::ostream
& out
) = 0;
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
;
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.
73 std::map
<Node
, Node
> d_fv_to_skolem
;
75 Node
convertToSkolem(Node n
);
76 /** initialize checker
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.
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.
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
92 void initializeChecker(std::unique_ptr
<SmtEngine
>& smte
,
94 ExprManagerMapCollection
& varMap
,
98 * Run the satisfiability check on query and return the result
99 * (sat/unsat/unknown).
101 * In contrast to the above method, this call should be used for cases where
102 * the model for the query is not important.
104 Result
doCheck(Node query
);
107 } // namespace quantifiers
108 } // namespace theory
111 #endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */