GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/candidate_rewrite_filter.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 2 4 50.0 %

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