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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
/********************* */
/*! \file candidate_rewrite_database.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 candidate_rewrite_database
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
#include <map>
#include <memory>
#include <unordered_set>
#include <vector>
#include "theory/quantifiers/candidate_rewrite_filter.h"
#include "theory/quantifiers/expr_miner.h"
#include "theory/quantifiers/sygus_sampler.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
/** CandidateRewriteDatabase
*
* This maintains the necessary data structures for generating a database
* of candidate rewrite rules (see Reynolds et al "Rewrites for SMT Solvers
* Using Syntax-Guided Enumeration" SMT 2018). The primary responsibilities
* of this class are to perform the "equivalence checking" and "congruence
* and matching filtering" in Figure 1. The equivalence checking is done
* through a combination of the sygus sampler object owned by this class
* and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
* rule filtering (based on congruence, matching, variable ordering) is also
* managed by the sygus sampler object.
*/
class CandidateRewriteDatabase : public ExprMiner
{
public:
CandidateRewriteDatabase();
~CandidateRewriteDatabase() {}
/** Initialize this class */
void initialize(const std::vector<Node>& var,
SygusSampler* ss = nullptr) override;
/** Initialize this class
*
* Serves the same purpose as the above function, but we will be using
* sygus to enumerate terms and generate samples.
*
* qe : pointer to quantifiers engine. We use the sygus term database of this
* quantifiers engine, and the extended rewriter of the corresponding term
* database when computing candidate rewrites,
* f : a term of some SyGuS datatype type whose values we will be
* testing under the free variables in the grammar of f. This is the
* "candidate variable" CegConjecture::d_candidates.
*/
void initializeSygus(const std::vector<Node>& vars,
QuantifiersEngine* qe,
Node f,
SygusSampler* ss = nullptr);
/** add term
*
* Notifies this class that the solution sol was enumerated. This may
* cause a candidate-rewrite to be printed on the output stream out.
* We return true if the term sol is distinct (up to equivalence) with
* all previous terms added to this class. The argument rew_print is set to
* true if this class printed a rewrite involving sol.
*
* If the flag rec is true, then we also recursively add all subterms of sol
* to this class as well.
*/
bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print);
bool addTerm(Node sol, bool rec, std::ostream& out);
bool addTerm(Node sol, std::ostream& out) override;
/** sets whether this class should output candidate rewrites it finds */
void setSilent(bool flag);
/** set the (extended) rewriter used by this class */
void setExtendedRewriter(ExtendedRewriter* er);
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
/** (required) pointer to the sygus term database of d_qe */
TermDbSygus* d_tds;
/** an extended rewriter object */
ExtendedRewriter* d_ext_rewrite;
/** the function-to-synthesize we are testing (if sygus) */
Node d_candidate;
/** whether we are using sygus */
bool d_using_sygus;
/** candidate rewrite filter */
CandidateRewriteFilter d_crewrite_filter;
/** the cache for results of addTerm */
std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache;
/** if true, we silence the output of candidate rewrites */
bool d_silent;
};
/**
* This class generates and stores candidate rewrite databases for multiple
* types as needed.
*/
class CandidateRewriteDatabaseGen
{
public:
/** constructor
*
* vars : the variables we are testing substitutions for, for all types,
* nsamples : number of sample points this class will test for all types.
*/
CandidateRewriteDatabaseGen(std::vector<Node>& vars, unsigned nsamples);
/** add term
*
* This registers term n with this class. We generate the candidate rewrite
* database of the appropriate type (if not allocated already), and register
* n with this database. This may result in "candidate-rewrite" being
* printed on the output stream out. We return true if the term sol is
* distinct (up to equivalence) with all previous terms added to this class.
*/
bool addTerm(Node n, std::ostream& out);
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
/** the variables */
std::vector<Node> d_vars;
/** sygus sampler object for each type */
std::map<TypeNode, SygusSampler> d_sampler;
/** the number of samples */
unsigned d_nsamples;
/** candidate rewrite databases for each type */
std::map<TypeNode, CandidateRewriteDatabase> d_cdbs;
/** an extended rewriter object */
ExtendedRewriter d_ext_rewrite;
};
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
|
