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