1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implements techniques for candidate rewrite rule filtering, which |
14 |
|
* filters the output of --sygus-rr-synth. The classes in this file implement |
15 |
|
* filtering based on congruence, variable ordering, and matching. |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "cvc5_private.h" |
19 |
|
|
20 |
|
#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H |
21 |
|
#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H |
22 |
|
|
23 |
|
#include <map> |
24 |
|
#include "expr/match_trie.h" |
25 |
|
#include "theory/quantifiers/dynamic_rewrite.h" |
26 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
27 |
|
#include "theory/quantifiers/sygus_sampler.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace quantifiers { |
32 |
|
|
33 |
|
/** candidate rewrite filter |
34 |
|
* |
35 |
|
* This class is responsible for various filtering techniques for candidate |
36 |
|
* rewrite rules, including: |
37 |
|
* (1) filtering based on variable ordering, |
38 |
|
* (2) filtering based on congruence, |
39 |
|
* (3) filtering based on matching. |
40 |
|
* For details, see Reynolds et al "Rewrites for SMT Solvers using Syntax-Guided |
41 |
|
* Enumeration", SMT 2018. |
42 |
|
* |
43 |
|
* In the following, we assume that the registerRelevantPair method of this |
44 |
|
* class been called for some pairs of terms. For each such call to |
45 |
|
* registerRelevantPair( t, s ), we say that (t,s) and (s,t) are "relevant |
46 |
|
* pairs". A relevant pair ( t, s ) typically corresponds to a (candidate) |
47 |
|
* rewrite t = s. |
48 |
|
*/ |
49 |
62 |
class CandidateRewriteFilter |
50 |
|
{ |
51 |
|
public: |
52 |
|
CandidateRewriteFilter(); |
53 |
|
|
54 |
|
/** initialize |
55 |
|
* |
56 |
|
* Initializes this class, ss is the sygus sampler that this class is |
57 |
|
* filtering rewrite rule pairs for, and tds is a point to the sygus term |
58 |
|
* database utility class. |
59 |
|
* |
60 |
|
* If useSygusType is false, this means that the terms in filterPair and |
61 |
|
* registerRelevantPair calls should be interpreted as themselves. Otherwise, |
62 |
|
* if useSygusType is true, these terms should be interpreted as their |
63 |
|
* analog according to the deep embedding. |
64 |
|
*/ |
65 |
|
void initialize(SygusSampler* ss, TermDbSygus* tds, bool useSygusType); |
66 |
|
/** filter pair |
67 |
|
* |
68 |
|
* This method returns true if the pair (n, eq_n) should be filtered. If it |
69 |
|
* is not filtered, then the caller may choose to call |
70 |
|
* registerRelevantPair(n, eq_n) below, although it may not, say if it finds |
71 |
|
* another reason to discard the pair. |
72 |
|
* |
73 |
|
* If this method returns false, then for all previous relevant pairs |
74 |
|
* ( a, eq_a ), we have that n = eq_n is not an instance of a = eq_a |
75 |
|
* modulo symmetry of equality, nor is n = eq_n derivable from the set of |
76 |
|
* all previous relevant pairs. The latter is determined by the d_drewrite |
77 |
|
* utility. For example: |
78 |
|
* [1] ( t+0, t ) and ( x+0, x ) |
79 |
|
* will not both be relevant pairs of this function since t+0=t is |
80 |
|
* an instance of x+0=x. |
81 |
|
* [2] ( s, t ) and ( s+0, t+0 ) |
82 |
|
* will not both be relevant pairs of this function since s+0=t+0 is |
83 |
|
* derivable from s=t. |
84 |
|
* These two criteria may be combined, for example: |
85 |
|
* [3] ( t+0, s ) is not a relevant pair if both ( x+0, x+s ) and ( t+s, s ) |
86 |
|
* are relevant pairs, since t+0 is an instance of x+0 where |
87 |
|
* { x |-> t }, and x+s { x |-> t } = s is derivable, via the third pair |
88 |
|
* above (t+s = s). |
89 |
|
*/ |
90 |
|
bool filterPair(Node n, Node eq_n); |
91 |
|
/** register relevant pair |
92 |
|
* |
93 |
|
* This should be called after filterPair( n, eq_n ) returns false. |
94 |
|
* This registers ( n, eq_n ) as a relevant pair with this class. |
95 |
|
*/ |
96 |
|
void registerRelevantPair(Node n, Node eq_n); |
97 |
|
|
98 |
|
private: |
99 |
|
/** pointer to the sygus sampler that this class is filtering rewrites for */ |
100 |
|
SygusSampler* d_ss; |
101 |
|
/** pointer to the sygus term database, used if d_use_sygus_type is true */ |
102 |
|
TermDbSygus* d_tds; |
103 |
|
/** whether we are registering sygus terms with this class */ |
104 |
|
bool d_use_sygus_type; |
105 |
|
|
106 |
|
//----------------------------congruence filtering |
107 |
|
/** a (dummy) user context, used for d_drewrite */ |
108 |
|
context::UserContext d_fake_context; |
109 |
|
/** dynamic rewriter class */ |
110 |
|
std::unique_ptr<DynamicRewriter> d_drewrite; |
111 |
|
//----------------------------end congruence filtering |
112 |
|
|
113 |
|
//----------------------------match filtering |
114 |
|
/** |
115 |
|
* Stores all relevant pairs returned by this sampler (see registerTerm). In |
116 |
|
* detail, if (t,s) is a relevant pair, then t in d_pairs[s]. |
117 |
|
*/ |
118 |
|
std::map<Node, std::unordered_set<Node> > d_pairs; |
119 |
|
/** |
120 |
|
* For each (builtin) type, a match trie storing all terms in the domain of |
121 |
|
* d_pairs. |
122 |
|
* |
123 |
|
* Notice that we store d_drewrite->toInternal(t) instead of t, for each |
124 |
|
* term t, so that polymorphism is handled properly. In particular, this |
125 |
|
* prevents matches between terms select( x, y ) and select( z, y ) where |
126 |
|
* the type of x and z are different. |
127 |
|
*/ |
128 |
|
std::map<TypeNode, expr::MatchTrie> d_match_trie; |
129 |
|
/** Notify class */ |
130 |
62 |
class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch |
131 |
|
{ |
132 |
|
CandidateRewriteFilter& d_sse; |
133 |
|
|
134 |
|
public: |
135 |
62 |
CandidateRewriteFilterNotifyMatch(CandidateRewriteFilter& sse) : d_sse(sse) |
136 |
|
{ |
137 |
62 |
} |
138 |
|
/** notify match */ |
139 |
80 |
bool notify(Node n, |
140 |
|
Node s, |
141 |
|
std::vector<Node>& vars, |
142 |
|
std::vector<Node>& subs) override |
143 |
|
{ |
144 |
80 |
return d_sse.notify(n, s, vars, subs); |
145 |
|
} |
146 |
|
}; |
147 |
|
/** Notify object used for reporting matches from d_match_trie */ |
148 |
|
CandidateRewriteFilterNotifyMatch d_ssenm; |
149 |
|
/** |
150 |
|
* Stores the current right hand side of a pair we are considering. |
151 |
|
* |
152 |
|
* In more detail, in registerTerm, we are interested in whether a pair (s,t) |
153 |
|
* is a relevant pair. We do this by: |
154 |
|
* (1) Setting the node d_curr_pair_rhs to t, |
155 |
|
* (2) Using d_match_trie, compute all terms s1...sn that match s. |
156 |
|
* For each si, where s = si * sigma for some substitution sigma, we check |
157 |
|
* whether t = ti * sigma for some previously relevant pair (si,ti), in |
158 |
|
* which case (s,t) is an instance of (si,ti). |
159 |
|
*/ |
160 |
|
Node d_curr_pair_rhs; |
161 |
|
/** |
162 |
|
* Called by the above class during d_match_trie.getMatches( s ), when we |
163 |
|
* find that si = s * sigma, where si is a term that is stored in |
164 |
|
* d_match_trie. |
165 |
|
* |
166 |
|
* This function returns false if ( s, d_curr_pair_rhs ) is an instance of |
167 |
|
* previously relevant pair. |
168 |
|
*/ |
169 |
|
bool notify(Node s, Node n, std::vector<Node>& vars, std::vector<Node>& subs); |
170 |
|
//----------------------------end match filtering |
171 |
|
}; |
172 |
|
|
173 |
|
} // namespace quantifiers |
174 |
|
} // namespace theory |
175 |
|
} // namespace cvc5 |
176 |
|
|
177 |
|
#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ |