GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/candidate_rewrite_database.cpp Lines: 88 132 66.7 %
Date: 2021-03-23 Branches: 143 480 29.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file candidate_rewrite_database.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli
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 Implementation of candidate_rewrite_database
13
 **/
14
15
#include "theory/quantifiers/candidate_rewrite_database.h"
16
17
#include "api/cvc4cpp.h"
18
#include "options/base_options.h"
19
#include "printer/printer.h"
20
#include "smt/smt_engine.h"
21
#include "smt/smt_engine_scope.h"
22
#include "smt/smt_statistics_registry.h"
23
#include "theory/quantifiers/sygus/term_database_sygus.h"
24
#include "theory/quantifiers/term_util.h"
25
#include "theory/quantifiers_engine.h"
26
#include "theory/rewriter.h"
27
28
using namespace std;
29
using namespace CVC4::kind;
30
using namespace CVC4::context;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace quantifiers {
35
36
12
CandidateRewriteDatabase::CandidateRewriteDatabase(bool doCheck,
37
                                                   bool rewAccel,
38
                                                   bool silent,
39
12
                                                   bool filterPairs)
40
    : d_qe(nullptr),
41
      d_tds(nullptr),
42
      d_ext_rewrite(nullptr),
43
      d_doCheck(doCheck),
44
      d_rewAccel(rewAccel),
45
      d_silent(silent),
46
      d_filterPairs(filterPairs),
47
12
      d_using_sygus(false)
48
{
49
12
}
50
void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
51
                                          SygusSampler* ss)
52
{
53
  Assert(ss != nullptr);
54
  d_candidate = Node::null();
55
  d_using_sygus = false;
56
  d_qe = nullptr;
57
  d_tds = nullptr;
58
  d_ext_rewrite = nullptr;
59
  if (d_filterPairs)
60
  {
61
    d_crewrite_filter.initialize(ss, nullptr, false);
62
  }
63
  ExprMiner::initialize(vars, ss);
64
}
65
66
8
void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
67
                                               QuantifiersEngine* qe,
68
                                               Node f,
69
                                               SygusSampler* ss)
70
{
71
8
  Assert(ss != nullptr);
72
8
  d_candidate = f;
73
8
  d_using_sygus = true;
74
8
  d_qe = qe;
75
8
  d_tds = d_qe->getTermDatabaseSygus();
76
8
  d_ext_rewrite = nullptr;
77
8
  if (d_filterPairs)
78
  {
79
8
    d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
80
  }
81
8
  ExprMiner::initialize(vars, ss);
82
8
}
83
84
1377
Node CandidateRewriteDatabase::addTerm(Node sol,
85
                                       bool rec,
86
                                       std::ostream& out,
87
                                       bool& rew_print)
88
{
89
  // have we added this term before?
90
  std::unordered_map<Node, Node, NodeHashFunction>::iterator itac =
91
1377
      d_add_term_cache.find(sol);
92
1377
  if (itac != d_add_term_cache.end())
93
  {
94
    return itac->second;
95
  }
96
97
1377
  if (rec)
98
  {
99
    // if recursive, we first add all subterms
100
    for (const Node& solc : sol)
101
    {
102
      // whether a candidate rewrite is printed for any subterm is irrelevant
103
      bool rew_printc = false;
104
      addTerm(solc, rec, out, rew_printc);
105
    }
106
  }
107
  // register the term
108
1377
  bool is_unique_term = true;
109
2754
  Node eq_sol = d_sampler->registerTerm(sol);
110
  // eq_sol is a candidate solution that is equivalent to sol
111
1377
  if (eq_sol != sol)
112
  {
113
313
    is_unique_term = false;
114
    // should we filter the pair?
115
313
    if (!d_filterPairs || !d_crewrite_filter.filterPair(sol, eq_sol))
116
    {
117
      // get the actual term
118
320
      Node solb = sol;
119
320
      Node eq_solb = eq_sol;
120
160
      if (d_using_sygus)
121
      {
122
160
        Assert(d_tds != nullptr);
123
160
        solb = d_tds->sygusToBuiltin(sol);
124
160
        eq_solb = d_tds->sygusToBuiltin(eq_sol);
125
      }
126
      // get the rewritten form
127
320
      Node solbr;
128
320
      Node eq_solr;
129
160
      if (d_ext_rewrite != nullptr)
130
      {
131
160
        solbr = d_ext_rewrite->extendedRewrite(solb);
132
160
        eq_solr = d_ext_rewrite->extendedRewrite(eq_solb);
133
      }
134
      else
135
      {
136
        solbr = Rewriter::rewrite(solb);
137
        eq_solr = Rewriter::rewrite(eq_solb);
138
      }
139
160
      bool verified = false;
140
160
      Trace("rr-check") << "Check candidate rewrite..." << std::endl;
141
      // verify it if applicable
142
160
      if (d_doCheck)
143
      {
144
232
        Node crr = solbr.eqNode(eq_solr).negate();
145
116
        Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
146
147
        // Notice we don't set produce-models. rrChecker takes the same
148
        // options as the SmtEngine we belong to, where we ensure that
149
        // produce-models is set.
150
232
        std::unique_ptr<SmtEngine> rrChecker;
151
116
        initializeChecker(rrChecker, crr);
152
232
        Result r = rrChecker->checkSat();
153
116
        Trace("rr-check") << "...result : " << r << std::endl;
154
116
        if (r.asSatisfiabilityResult().isSat() == Result::SAT)
155
        {
156
14
          Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
157
14
          is_unique_term = true;
158
28
          std::vector<Node> vars;
159
14
          d_sampler->getVariables(vars);
160
28
          std::vector<Node> pt;
161
56
          for (const Node& v : vars)
162
          {
163
84
            Node val;
164
84
            Node refv = v;
165
            // if a bound variable, map to the skolem we introduce before
166
            // looking up the model value
167
42
            if (v.getKind() == BOUND_VARIABLE)
168
            {
169
42
              std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
170
42
              if (itf == d_fv_to_skolem.end())
171
              {
172
                // not in conjecture, can use arbitrary value
173
13
                val = v.getType().mkGroundTerm();
174
              }
175
              else
176
              {
177
                // get the model value of its skolem
178
29
                refv = itf->second;
179
              }
180
            }
181
42
            if (val.isNull())
182
            {
183
29
              Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
184
29
              val = rrChecker->getValue(refv);
185
            }
186
42
            Trace("rr-check") << "  " << v << " -> " << val << std::endl;
187
42
            pt.push_back(val);
188
          }
189
14
          d_sampler->addSamplePoint(pt);
190
          // add the solution again
191
          // by construction of the above point, we should be unique now
192
14
          eq_sol = d_sampler->registerTerm(sol);
193
14
          Assert(eq_sol == sol);
194
        }
195
        else
196
        {
197
102
          verified = !r.asSatisfiabilityResult().isUnknown();
198
        }
199
      }
200
      else
201
      {
202
        // just insist that constants are not relevant pairs
203
44
        if (solb.isConst() && eq_solb.isConst())
204
        {
205
          is_unique_term = true;
206
          eq_sol = sol;
207
        }
208
      }
209
160
      if (!is_unique_term)
210
      {
211
        // register this as a relevant pair (helps filtering)
212
146
        if (d_filterPairs)
213
        {
214
146
          d_crewrite_filter.registerRelevantPair(sol, eq_sol);
215
        }
216
        // The analog of terms sol and eq_sol are equivalent under
217
        // sample points but do not rewrite to the same term. Hence,
218
        // this indicates a candidate rewrite.
219
146
        if (!d_silent)
220
        {
221
146
          out << "(" << (verified ? "" : "candidate-") << "rewrite ";
222
146
          if (d_using_sygus)
223
          {
224
146
            TermDbSygus::toStreamSygus(out, sol);
225
146
            out << " ";
226
146
            TermDbSygus::toStreamSygus(out, eq_sol);
227
          }
228
          else
229
          {
230
            out << sol << " " << eq_sol;
231
          }
232
146
          out << ")" << std::endl;
233
        }
234
        // we count this as printed, despite not literally printing it
235
146
        rew_print = true;
236
        // debugging information
237
146
        if (Trace.isOn("sygus-rr-debug"))
238
        {
239
          Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr
240
                                  << std::endl;
241
          Trace("sygus-rr-debug")
242
              << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
243
        }
244
146
        if (d_rewAccel && d_using_sygus)
245
        {
246
          Assert(d_tds != nullptr);
247
          // Add a symmetry breaking clause that excludes the larger
248
          // of sol and eq_sol. This effectively states that we no longer
249
          // wish to enumerate any term that contains sol (resp. eq_sol)
250
          // as a subterm.
251
          Node exc_sol = sol;
252
          unsigned sz = d_tds->getSygusTermSize(sol);
253
          unsigned eqsz = d_tds->getSygusTermSize(eq_sol);
254
          if (eqsz > sz)
255
          {
256
            sz = eqsz;
257
            exc_sol = eq_sol;
258
          }
259
          TypeNode ptn = d_candidate.getType();
260
          Node x = d_tds->getFreeVar(ptn, 0);
261
          Node lem = d_tds->getExplain()->getExplanationForEquality(x, exc_sol);
262
          lem = lem.negate();
263
          Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem
264
                               << std::endl;
265
          d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz);
266
        }
267
      }
268
    }
269
    // We count this as a rewrite if we did not explicitly rule it out.
270
    // The value of is_unique_term is false iff this call resulted in a rewrite.
271
    // Notice that when --sygus-rr-synth-check is enabled,
272
    // statistics on number of candidate rewrite rules is
273
    // an accurate count of (#enumerated_terms-#unique_terms) only if
274
    // the option sygus-rr-synth-filter-order is disabled. The reason
275
    // is that the sygus sampler may reason that a candidate rewrite
276
    // rule is not useful since its variables are unordered, whereby
277
    // it discards it as a redundant candidate rewrite rule before
278
    // checking its correctness.
279
  }
280
1377
  d_add_term_cache[sol] = eq_sol;
281
1377
  return eq_sol;
282
}
283
284
Node CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out)
285
{
286
  bool rew_print = false;
287
  return addTerm(sol, rec, out, rew_print);
288
}
289
bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
290
{
291
  Node rsol = addTerm(sol, false, out);
292
  return sol == rsol;
293
}
294
295
8
void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; }
296
297
8
void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er)
298
{
299
8
  d_ext_rewrite = er;
300
8
}
301
302
} /* CVC4::theory::quantifiers namespace */
303
} /* CVC4::theory namespace */
304
26685
} /* CVC4 namespace */