GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/candidate_rewrite_filter.cpp Lines: 115 126 91.3 %
Date: 2021-03-22 Branches: 269 630 42.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file candidate_rewrite_filter.cpp
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 "theory/quantifiers/candidate_rewrite_filter.h"
18
19
#include "options/base_options.h"
20
#include "options/quantifiers_options.h"
21
#include "printer/printer.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
// the number of d_drewrite objects we have allocated (to avoid name conflicts)
30
static unsigned drewrite_counter = 0;
31
32
12
CandidateRewriteFilter::CandidateRewriteFilter()
33
    : d_ss(nullptr),
34
      d_tds(nullptr),
35
      d_use_sygus_type(false),
36
      d_drewrite(nullptr),
37
12
      d_ssenm(*this)
38
{
39
12
}
40
41
8
void CandidateRewriteFilter::initialize(SygusSampler* ss,
42
                                        TermDbSygus* tds,
43
                                        bool useSygusType)
44
{
45
8
  d_ss = ss;
46
8
  d_use_sygus_type = useSygusType;
47
8
  d_tds = tds;
48
  // initialize members of this class
49
8
  d_match_trie.clear();
50
8
  d_pairs.clear();
51
  // (re)initialize the dynamic rewriter
52
16
  std::stringstream ssn;
53
8
  ssn << "_dyn_rewriter_" << drewrite_counter;
54
8
  drewrite_counter++;
55
24
  d_drewrite = std::unique_ptr<DynamicRewriter>(
56
32
      new DynamicRewriter(ssn.str(), &d_fake_context));
57
8
}
58
59
313
bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
60
{
61
626
  Node bn = n;
62
626
  Node beq_n = eq_n;
63
313
  if (d_use_sygus_type)
64
  {
65
313
    bn = d_tds->sygusToBuiltin(n);
66
313
    beq_n = d_tds->sygusToBuiltin(eq_n);
67
  }
68
626
  Trace("cr-filter") << "crewriteFilter : " << bn << "..." << beq_n
69
313
                     << std::endl;
70
  // whether we will keep this pair
71
313
  bool keep = true;
72
73
  // ----- check redundancy based on variables
74
1565
  if (options::sygusRewSynthFilterOrder()
75
939
      || options::sygusRewSynthFilterNonLinear())
76
  {
77
1252
    bool nor = d_ss->checkVariables(bn,
78
313
                                    options::sygusRewSynthFilterOrder(),
79
626
                                    options::sygusRewSynthFilterNonLinear());
80
1252
    bool eqor = d_ss->checkVariables(beq_n,
81
313
                                     options::sygusRewSynthFilterOrder(),
82
626
                                     options::sygusRewSynthFilterNonLinear());
83
626
    Trace("cr-filter-debug")
84
313
        << "Variables ok? : " << nor << " " << eqor << std::endl;
85
313
    if (eqor || nor)
86
    {
87
      // if only one is ordered, then we require that the ordered one's
88
      // variables cannot be a strict subset of the variables of the other.
89
486
      if (!eqor)
90
      {
91
4
        if (d_ss->containsFreeVariables(beq_n, bn, true))
92
        {
93
1
          keep = false;
94
        }
95
        else
96
        {
97
          // if the previous value stored was unordered, but n is
98
          // ordered, we prefer n. Thus, we force its addition to the
99
          // sampler database.
100
3
          d_ss->registerTerm(n, true);
101
        }
102
      }
103
239
      else if (!nor)
104
      {
105
86
        keep = !d_ss->containsFreeVariables(bn, beq_n, true);
106
      }
107
    }
108
    else
109
    {
110
70
      keep = false;
111
    }
112
313
    if (!keep)
113
    {
114
147
      Trace("cr-filter") << "...redundant (unordered)" << std::endl;
115
    }
116
  }
117
118
  // ----- check rewriting redundancy
119
1492
  if (keep && options::sygusRewSynthFilterCong())
120
  {
121
    // When using sygus types, this filtering applies to the builtin versions
122
    // of n and eq_n. This means that we may filter out a rewrite rule for one
123
    // sygus type based on another, e.g. we won't report x=x+0 for both A and B
124
    // in:
125
    //   A -> x | 0 | A+A
126
    //   B -> x | 0 | B+B
127
166
    Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl;
128
166
    if (d_drewrite->areEqual(bn, beq_n))
129
    {
130
      // must be unique according to the dynamic rewriter
131
3
      Trace("cr-filter") << "...redundant (rewritable)" << std::endl;
132
3
      keep = false;
133
    }
134
  }
135
136
625
  if (keep && options::sygusRewSynthFilterMatch())
137
  {
138
    // ----- check matchable
139
    // check whether the pair is matchable with a previous one
140
163
    d_curr_pair_rhs = beq_n;
141
326
    Trace("crf-match") << "CRF check matches : " << bn << " [rhs = " << beq_n
142
163
                       << "]..." << std::endl;
143
326
    Node bni = d_drewrite->toInternal(bn);
144
163
    if (!bni.isNull())
145
    {
146
      // as with congruence filtering, we cache based on the builtin type
147
326
      TypeNode tn = bn.getType();
148
163
      if (!d_match_trie[tn].getMatches(bni, &d_ssenm))
149
      {
150
3
        keep = false;
151
3
        Trace("cr-filter") << "...redundant (matchable)" << std::endl;
152
        // regardless, would help to remember it
153
3
        registerRelevantPair(n, eq_n);
154
      }
155
    }
156
    // if bni is null, it may involve non-first-class types that we cannot
157
    // reason about
158
  }
159
160
313
  if (keep)
161
  {
162
160
    return false;
163
  }
164
153
  if (Trace.isOn("sygus-rr-filter"))
165
  {
166
    std::stringstream ss;
167
    ss << "(redundant-rewrite ";
168
    TermDbSygus::toStreamSygus(ss, n);
169
    ss << " ";
170
    TermDbSygus::toStreamSygus(ss, eq_n);
171
    ss << ")";
172
    Trace("sygus-rr-filter") << ss.str() << std::endl;
173
  }
174
153
  return true;
175
}
176
177
149
void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
178
{
179
298
  Node bn = n;
180
298
  Node beq_n = eq_n;
181
149
  if (d_use_sygus_type)
182
  {
183
149
    bn = d_tds->sygusToBuiltin(n);
184
149
    beq_n = d_tds->sygusToBuiltin(eq_n);
185
  }
186
  // ----- check rewriting redundancy
187
149
  if (options::sygusRewSynthFilterCong())
188
  {
189
149
    Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
190
149
    Assert(!d_drewrite->areEqual(bn, beq_n));
191
149
    d_drewrite->addRewrite(bn, beq_n);
192
  }
193
149
  if (options::sygusRewSynthFilterMatch())
194
  {
195
    // cache based on the builtin type
196
298
    TypeNode tn = bn.getType();
197
    // add to match information
198
447
    for (unsigned r = 0; r < 2; r++)
199
    {
200
596
      Node t = r == 0 ? bn : beq_n;
201
596
      Node to = r == 0 ? beq_n : bn;
202
      // insert in match trie if first time
203
298
      if (d_pairs.find(t) == d_pairs.end())
204
      {
205
210
        Trace("crf-match") << "CRF add term : " << t << std::endl;
206
420
        Node ti = d_drewrite->toInternal(t);
207
210
        if (!ti.isNull())
208
        {
209
210
          d_match_trie[tn].addTerm(ti);
210
        }
211
      }
212
298
      d_pairs[t].insert(to);
213
    }
214
  }
215
149
}
216
217
120
bool CandidateRewriteFilter::notify(Node s,
218
                                    Node n,
219
                                    std::vector<Node>& vars,
220
                                    std::vector<Node>& subs)
221
{
222
120
  Trace("crf-match-debug") << "Got : " << s << " matches " << n << std::endl;
223
120
  Assert(!d_curr_pair_rhs.isNull());
224
  // convert back to original forms
225
120
  s = d_drewrite->toExternal(s);
226
120
  Assert(!s.isNull());
227
120
  n = d_drewrite->toExternal(n);
228
120
  Assert(!n.isNull());
229
  std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
230
120
      d_pairs.find(n);
231
120
  if (Trace.isOn("crf-match"))
232
  {
233
    Trace("crf-match") << "  " << s << " matches " << n
234
                       << " under:" << std::endl;
235
    for (unsigned i = 0, size = vars.size(); i < size; i++)
236
    {
237
      Trace("crf-match") << "    " << vars[i] << " -> " << subs[i] << std::endl;
238
    }
239
  }
240
#ifdef CVC4_ASSERTIONS
241
246
  for (unsigned i = 0, size = vars.size(); i < size; i++)
242
  {
243
    // By using internal representation of terms, we ensure polymorphism is
244
    // handled correctly.
245
126
    Assert(vars[i].getType().isComparableTo(subs[i].getType()));
246
  }
247
#endif
248
  // must convert the inferred substitution to original form
249
240
  std::vector<Node> esubs;
250
246
  for (const Node& sb : subs)
251
  {
252
126
    esubs.push_back(d_drewrite->toExternal(sb));
253
  }
254
120
  Assert(it != d_pairs.end());
255
984
  for (const Node& nr : it->second)
256
  {
257
    Node nrs =
258
1731
        nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end());
259
867
    bool areEqual = (nrs == d_curr_pair_rhs);
260
867
    if (!areEqual && options::sygusRewSynthFilterCong())
261
    {
262
      // if dynamic rewriter is available, consult it
263
864
      areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
264
    }
265
867
    if (areEqual)
266
    {
267
3
      Trace("crf-match") << "*** Match, current pair: " << std::endl;
268
6
      Trace("crf-match") << "  (" << s << ", " << d_curr_pair_rhs << ")"
269
3
                         << std::endl;
270
3
      Trace("crf-match") << "is an instance of previous pair:" << std::endl;
271
3
      Trace("crf-match") << "  (" << n << ", " << nr << ")" << std::endl;
272
3
      return false;
273
    }
274
  }
275
117
  return true;
276
}
277
278
}  // namespace quantifiers
279
}  // namespace theory
280
29732
}  // namespace CVC4