GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_norm.cpp Lines: 126 256 49.2 %
Date: 2021-03-22 Branches: 223 1098 20.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_norm.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Tim King
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 class for for simplifying SyGuS grammars after they
13
 ** are encoded into datatypes.
14
 **/
15
16
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
17
18
#include "expr/dtype_cons.h"
19
#include "expr/node_manager_attributes.h"  // for VarNameAttr
20
#include "options/quantifiers_options.h"
21
#include "smt/smt_engine.h"
22
#include "smt/smt_engine_scope.h"
23
#include "theory/datatypes/theory_datatypes_utils.h"
24
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
25
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
26
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
27
#include "theory/quantifiers/sygus/term_database_sygus.h"
28
#include "theory/quantifiers/term_util.h"
29
30
#include <numeric>  // for std::iota
31
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace quantifiers {
37
38
34051
bool OpPosTrie::getOrMakeType(TypeNode tn,
39
                              TypeNode& unres_tn,
40
                              const std::vector<unsigned>& op_pos,
41
                              unsigned ind)
42
{
43
34051
  if (ind == op_pos.size())
44
  {
45
    /* Found type */
46
3765
    if (!d_unres_tn.isNull())
47
    {
48
6072
      Trace("sygus-grammar-normalize-trie")
49
3036
          << "\tFound type " << d_unres_tn << "\n";
50
3036
      unres_tn = d_unres_tn;
51
3036
      return true;
52
    }
53
    /* Creating unresolved type */
54
1458
    std::stringstream ss;
55
729
    ss << tn << "_";
56
4158
    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
57
    {
58
3429
      ss << "_" << std::to_string(op_pos[i]);
59
    }
60
2187
    d_unres_tn = NodeManager::currentNM()->mkSort(
61
2187
        ss.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
62
1458
    Trace("sygus-grammar-normalize-trie")
63
729
        << "\tCreating type " << d_unres_tn << "\n";
64
729
    unres_tn = d_unres_tn;
65
729
    return false;
66
  }
67
  /* Go to next node */
68
30286
  return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
69
}
70
71
329
SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {}
72
73
729
SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
74
    : d_tn(src_tn),
75
      d_unres_tn(unres_tn),
76
729
      d_sdt(unres_tn.getAttribute(expr::VarNameAttr()))
77
{
78
729
}
79
80
3390
void SygusGrammarNorm::TypeObject::addConsInfo(
81
    SygusGrammarNorm* sygus_norm,
82
    const DTypeConstructor& cons)
83
{
84
3390
  Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
85
  /* Recover the sygus operator to not lose reference to the original
86
   * operator (NOT, ITE, etc) */
87
6780
  Node sygus_op = cons.getSygusOp();
88
6780
  Trace("sygus-grammar-normalize-debug")
89
3390
      << ".....operator is " << sygus_op << std::endl;
90
91
6780
  std::vector<TypeNode> consTypes;
92
3390
  const std::vector<std::shared_ptr<DTypeSelector> >& args = cons.getArgs();
93
6826
  for (const std::shared_ptr<DTypeSelector>& arg : args)
94
  {
95
    // Collect unresolved type nodes corresponding to the typenode of the
96
    // arguments.
97
6872
    TypeNode atype = arg->getRangeType();
98
    // normalize it recursively
99
3436
    atype = sygus_norm->normalizeSygusRec(atype);
100
3436
    consTypes.push_back(atype);
101
  }
102
103
6780
  d_sdt.addConstructor(
104
3390
      sygus_op, cons.getName(), consTypes, cons.getWeight());
105
3390
}
106
107
729
void SygusGrammarNorm::TypeObject::initializeDatatype(
108
    SygusGrammarNorm* sygus_norm, const DType& dt)
109
{
110
  /* Use the sygus type to not lose reference to the original types (Bool,
111
   * Int, etc) */
112
1458
  TypeNode sygusType = dt.getSygusType();
113
2187
  d_sdt.initializeDatatype(sygusType,
114
                           sygus_norm->d_sygus_vars,
115
729
                           dt.getSygusAllowConst(),
116
729
                           dt.getSygusAllowAll());
117
1458
  Trace("sygus-grammar-normalize")
118
729
      << "...built datatype " << d_sdt.getDatatype() << " ";
119
  /* Add to global accumulators */
120
729
  sygus_norm->d_dt_all.push_back(d_sdt.getDatatype());
121
729
  sygus_norm->d_unres_t_all.insert(d_unres_tn);
122
729
  Trace("sygus-grammar-normalize") << "---------------------------------\n";
123
729
}
124
125
27
void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm,
126
                                             TypeObject& to,
127
                                             const DType& dt,
128
                                             std::vector<unsigned>& op_pos)
129
{
130
54
  std::vector<unsigned> difference;
131
27
  std::set_difference(op_pos.begin(),
132
                      op_pos.end(),
133
                      d_drop_indices.begin(),
134
                      d_drop_indices.end(),
135
27
                      std::back_inserter(difference));
136
27
  op_pos = difference;
137
27
}
138
139
/* TODO #1304: have more operators and types. Moreover, have more general ways
140
   of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
141
   function should realize that it is chainable for integers */
142
bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op)
143
{
144
  /* Checks whether operator occurs chainable for its type */
145
  if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS)
146
  {
147
    return true;
148
  }
149
  return false;
150
}
151
152
/* TODO #1304: have more operators and types. Moreover, have more general ways
153
   of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
154
   function should realize that it is chainable for integers */
155
bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n)
156
{
157
  if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS
158
      && n == TermUtil::mkTypeValue(tn, 0))
159
  {
160
    return true;
161
  }
162
  return false;
163
}
164
165
void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
166
                                              TypeObject& to,
167
                                              const DType& dt,
168
                                              std::vector<unsigned>& op_pos)
169
{
170
  NodeManager* nm = NodeManager::currentNM();
171
  std::vector<unsigned> claimed(d_elem_pos);
172
  claimed.push_back(d_chain_op_pos);
173
  unsigned nb_op_pos = op_pos.size();
174
  /* TODO do this properly */
175
  /* Remove from op_pos the positions claimed by the transformation */
176
  std::sort(op_pos.begin(), op_pos.end());
177
  std::sort(claimed.begin(), claimed.end());
178
  std::vector<unsigned> difference;
179
  std::set_difference(op_pos.begin(),
180
                      op_pos.end(),
181
                      claimed.begin(),
182
                      claimed.end(),
183
                      std::back_inserter(difference));
184
  op_pos = difference;
185
  if (Trace.isOn("sygus-grammar-normalize-chain"))
186
  {
187
    Trace("sygus-grammar-normalize-chain")
188
        << "OP at " << d_chain_op_pos << "\n"
189
        << d_elem_pos.size() << " d_elem_pos: ";
190
    for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
191
    {
192
      Trace("sygus-grammar-normalize-chain") << d_elem_pos[i] << " ";
193
    }
194
    Trace("sygus-grammar-normalize-chain")
195
        << "\n"
196
        << op_pos.size() << " remaining op_pos: ";
197
    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
198
    {
199
      Trace("sygus-grammar-normalize-chain") << op_pos[i] << " ";
200
    }
201
    Trace("sygus-grammar-normalize-chain") << "\n";
202
  }
203
  /* Build identity operator and empty callback */
204
  Node iden_op = SygusGrammarNorm::getIdOp(dt.getSygusType());
205
  /* If all operators are claimed, create a monomial */
206
  if (nb_op_pos == d_elem_pos.size() + 1)
207
  {
208
    Trace("sygus-grammar-normalize-chain")
209
        << "\tCreating id type for " << d_elem_pos.back() << "\n";
210
    /* creates type for element */
211
    std::vector<unsigned> tmp;
212
    tmp.push_back(d_elem_pos.back());
213
    TypeNode t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp);
214
    /* consumes element */
215
    d_elem_pos.pop_back();
216
    /* adds to Root: "type" */
217
    std::vector<TypeNode> ctypes;
218
    ctypes.push_back(t);
219
    to.d_sdt.addConstructor(iden_op,
220
                            "id",
221
                            ctypes,
222
                            0);
223
    Trace("sygus-grammar-normalize-chain")
224
        << "\tAdding  " << t << " to " << to.d_unres_tn << "\n";
225
    /* adds to Root: "type + Root" */
226
    std::vector<TypeNode> ctypesp;
227
    ctypesp.push_back(t);
228
    ctypesp.push_back(to.d_unres_tn);
229
    to.d_sdt.addConstructor(nm->operatorOf(PLUS), kindToString(PLUS), ctypesp);
230
    Trace("sygus-grammar-normalize-chain")
231
        << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
232
        << to.d_unres_tn << " and " << t << "\n";
233
  }
234
  /* In the initial case if not all operators claimed always creates a next */
235
  Assert(nb_op_pos != d_elem_pos.size() + 1 || d_elem_pos.size() > 1);
236
  /* TODO #1304: consider case in which CHAIN op has different types than
237
     to.d_tn */
238
  /* If no more elements to chain, finish */
239
  if (d_elem_pos.size() == 0)
240
  {
241
    return;
242
  }
243
  /* Creates a type do be added to root representing next step in the chain */
244
  /* Add + to elems */
245
  d_elem_pos.push_back(d_chain_op_pos);
246
  if (Trace.isOn("sygus-grammar-normalize-chain"))
247
  {
248
    Trace("sygus-grammar-normalize-chain")
249
        << "\tCreating type for next entry with sygus_ops ";
250
    for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
251
    {
252
      Trace("sygus-grammar-normalize-chain")
253
          << dt[d_elem_pos[i]].getSygusOp() << " ";
254
    }
255
    Trace("sygus-grammar-normalize-chain") << "\n";
256
  }
257
  /* adds to Root: (\lambda x. x ) Next */
258
  std::vector<TypeNode> ctypes;
259
  ctypes.push_back(sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos));
260
  to.d_sdt.addConstructor(iden_op,
261
                          "id_next",
262
                          ctypes,
263
                          0);
264
}
265
266
8892
std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
267
268
/* Traverse the constructors of dt according to the positions in op_pos. Collect
269
 * those that fit the kinds established by to_collect. Remove collected operator
270
 * positions from op_pos. Accumulate collected positions in collected
271
 *
272
 * returns true if collected anything
273
 */
274
729
std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
275
    TypeNode tn, const DType& dt, const std::vector<unsigned>& op_pos)
276
{
277
729
  NodeManager* nm = NodeManager::currentNM();
278
1458
  TypeNode sygus_tn = dt.getSygusType();
279
1458
  Trace("sygus-gnorm") << "Infer transf for " << dt.getName() << "..."
280
729
                       << std::endl;
281
1458
  Trace("sygus-gnorm") << "  #cons = " << op_pos.size() << " / "
282
729
                       << dt.getNumConstructors() << std::endl;
283
  // look for redundant constructors to drop
284
1458
  if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
285
  {
286
1431
    SygusRedundantCons src;
287
729
    src.initialize(d_tds, tn);
288
1431
    std::vector<unsigned> rindices;
289
729
    src.getRedundant(rindices);
290
729
    if (!rindices.empty())
291
    {
292
54
      Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/"
293
27
                           << op_pos.size() << " constructors." << std::endl;
294
27
      Assert(rindices.size() < op_pos.size());
295
27
      return std::unique_ptr<Transf>(new TransfDrop(rindices));
296
    }
297
  }
298
299
  // if normalization option is not enabled, we do not infer the transformations
300
  // below
301
1404
  if (!options::sygusGrammarNorm())
302
  {
303
702
    return nullptr;
304
  }
305
306
  /* TODO #1304: step 1: look for singleton */
307
  /* step 2: look for chain */
308
  unsigned chain_op_pos = dt.getNumConstructors();
309
  std::vector<unsigned> elem_pos;
310
  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
311
  {
312
    Assert(op_pos[i] < dt.getNumConstructors());
313
    Node sop = dt[op_pos[i]].getSygusOp();
314
    /* Collects a chainable operator such as PLUS */
315
    if (sop.getKind() == BUILTIN && TransfChain::isChainable(sygus_tn, sop))
316
    {
317
      Assert(nm->operatorToKind(sop) == PLUS);
318
      /* TODO #1304: be robust for this case */
319
      /* For now only transforms applications whose arguments have the same type
320
       * as the root */
321
      bool same_type_plus = true;
322
      const std::vector<std::shared_ptr<DTypeSelector> >& args =
323
          dt[op_pos[i]].getArgs();
324
      for (const std::shared_ptr<DTypeSelector>& arg : args)
325
      {
326
        if (arg->getRangeType() != tn)
327
        {
328
          same_type_plus = false;
329
          break;
330
        }
331
      }
332
      if (!same_type_plus)
333
      {
334
        Trace("sygus-grammar-normalize-infer")
335
            << "\tFor OP " << PLUS << " did not collecting sop " << sop
336
            << " in position " << op_pos[i] << "\n";
337
        continue;
338
      }
339
      Assert(chain_op_pos == dt.getNumConstructors());
340
      Trace("sygus-grammar-normalize-infer")
341
          << "\tCollecting chainable OP " << sop << " in position " << op_pos[i]
342
          << "\n";
343
      chain_op_pos = op_pos[i];
344
      continue;
345
    }
346
    /* TODO #1304: check this for each operator */
347
    /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
348
    if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), sop))
349
    {
350
      Trace("sygus-grammar-normalize-infer")
351
          << "\tCollecting for NON_ID_ELEMS the sop " << sop
352
          << " in position " << op_pos[i] << "\n";
353
      elem_pos.push_back(op_pos[i]);
354
    }
355
  }
356
  /* Typenode admits a chain transformation for normalization */
357
  if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
358
  {
359
    Trace("sygus-gnorm") << "...chain transf." << std::endl;
360
    Trace("sygus-grammar-normalize-infer")
361
        << "\tInfering chain transformation\n";
362
    return std::unique_ptr<Transf>(new TransfChain(chain_op_pos, elem_pos));
363
  }
364
  return nullptr;
365
}
366
367
3765
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
368
                                             const DType& dt,
369
                                             std::vector<unsigned>& op_pos)
370
{
371
3765
  Assert(tn.isDatatype());
372
  /* Corresponding type node to tn with the given operator positions. To be
373
   * retrieved (if cached) or defined (otherwise) */
374
3765
  TypeNode unres_tn;
375
3765
  if (Trace.isOn("sygus-grammar-normalize-trie"))
376
  {
377
    Trace("sygus-grammar-normalize-trie")
378
        << "\tRecursing on " << tn << " with op_positions ";
379
    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
380
    {
381
      Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
382
    }
383
    Trace("sygus-grammar-normalize-trie") << "\n";
384
  }
385
  /* Checks if unresolved type already created (and returns) or creates it
386
   * (and then proceeds to definition) */
387
3765
  std::sort(op_pos.begin(), op_pos.end());
388
3765
  if (d_tries[tn].getOrMakeType(tn, unres_tn, op_pos))
389
  {
390
3036
    if (Trace.isOn("sygus-grammar-normalize-trie"))
391
    {
392
      Trace("sygus-grammar-normalize-trie")
393
          << "\tTypenode " << tn << " has already been normalized with op_pos ";
394
      for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
395
      {
396
        Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
397
      }
398
      Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn << "\n";
399
    }
400
3036
    return unres_tn;
401
  }
402
729
  if (Trace.isOn("sygus-grammar-normalize-trie"))
403
  {
404
    Trace("sygus-grammar-normalize-trie")
405
        << "\tTypenode " << tn << " not yet normalized with op_pos ";
406
    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
407
    {
408
      Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
409
    }
410
    Trace("sygus-grammar-normalize-trie") << "\n";
411
  }
412
  /* Creates type object for normalization */
413
1458
  TypeObject to(tn, unres_tn);
414
415
729
  if (dt.getSygusAllowConst())
416
  {
417
114
    TypeNode sygus_type = dt.getSygusType();
418
    // must be handled by counterexample-guided instantiation
419
    // don't do it for Boolean (not worth the trouble, since it has only
420
    // minimal gain (1 any constant vs 2 constructors for true/false), and
421
    // we need to do a lot of special symmetry breaking, e.g. for ensuring
422
    // any constant constructors are not the 1st children of ITEs.
423
171
    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
424
171
        && !sygus_type.isBoolean())
425
    {
426
42
      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
427
84
      TypeNode dtn = dt.getSygusType();
428
      // we add this constructor first since we use left associative chains
429
      // and our symmetry breaking should group any constants together
430
      // beneath the same application
431
      // we set its weight to zero since it should be considered at the
432
      // same level as constants.
433
42
      to.d_sdt.addAnyConstantConstructor(dtn);
434
    }
435
    else
436
    {
437
      // add default constant constructors
438
30
      std::vector<Node> ops;
439
15
      CegGrammarConstructor::mkSygusConstantsForType(sygus_type, ops);
440
43
      for (const Node& op : ops)
441
      {
442
56
        std::stringstream ss;
443
28
        ss << op;
444
56
        std::vector<TypeNode> ctypes;
445
28
        to.d_sdt.addConstructor(op, ss.str(), ctypes);
446
      }
447
    }
448
  }
449
450
  /* Determine normalization transformation based on sygus type and given
451
    * operators */
452
1458
  std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
453
  /* If a transformation was selected, apply it */
454
729
  if (transformation != nullptr)
455
  {
456
27
    transformation->buildType(this, to, dt, op_pos);
457
  }
458
459
  // Remaining operators are rebuilt as they are.
460
  // Notice that we must extract the Datatype here to get the (Expr-layer)
461
  // sygus print callback.
462
4119
  for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
463
  {
464
3390
    unsigned oi = op_pos[i];
465
3390
    Assert(oi < dt.getNumConstructors());
466
3390
    to.addConsInfo(this, dt[oi]);
467
  }
468
  /* Build normalize datatype */
469
729
  if (Trace.isOn("sygus-grammar-normalize"))
470
  {
471
    Trace("sygus-grammar-normalize") << "\nFor positions ";
472
    for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
473
    {
474
      Trace("sygus-grammar-normalize") << op_pos[i] << " ";
475
    }
476
    Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
477
  }
478
729
  to.initializeDatatype(this, dt);
479
729
  return unres_tn;
480
}
481
482
3765
TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
483
{
484
3765
  if (!tn.isDatatype())
485
  {
486
    // Might not be a sygus datatype, e.g. if the input grammar had the
487
    // any constant constructor.
488
    return tn;
489
  }
490
  /* Collect all operators for normalization */
491
3765
  const DType& dt = tn.getDType();
492
3765
  if (!dt.isSygus())
493
  {
494
    // datatype but not sygus datatype case
495
    return tn;
496
  }
497
7530
  std::vector<unsigned> op_pos(dt.getNumConstructors());
498
3765
  std::iota(op_pos.begin(), op_pos.end(), 0);
499
3765
  return normalizeSygusRec(tn, dt, op_pos);
500
}
501
502
329
TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
503
{
504
  /* Normalize all types in tn */
505
329
  d_sygus_vars = sygus_vars;
506
329
  normalizeSygusRec(tn);
507
  /* Resolve created types */
508
329
  Assert(!d_dt_all.empty() && !d_unres_t_all.empty());
509
329
  if (Trace.isOn("sygus-grammar-normalize-build"))
510
  {
511
    Trace("sygus-grammar-normalize-build")
512
        << "making mutual datatyes with datatypes \n";
513
    for (unsigned i = 0, size = d_dt_all.size(); i < size; ++i)
514
    {
515
      Trace("sygus-grammar-normalize-build") << d_dt_all[i];
516
    }
517
    Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
518
    for (const TypeNode& unres_t : d_unres_t_all)
519
    {
520
      Trace("sygus-grammar-normalize-build") << unres_t << " ";
521
    }
522
    Trace("sygus-grammar-normalize-build") << "\n";
523
  }
524
329
  Assert(d_dt_all.size() == d_unres_t_all.size());
525
  std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
526
658
      d_dt_all, d_unres_t_all, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
527
329
  Assert(types.size() == d_dt_all.size());
528
  /* Clear accumulators */
529
329
  d_dt_all.clear();
530
329
  d_unres_t_all.clear();
531
  /* By construction the normalized type node will be the last one considered */
532
658
  return types.back();
533
}
534
535
}  // namespace quantifiers
536
}  // namespace theory
537
28107
}  // namespace CVC4