GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/term_database_sygus.cpp Lines: 479 553 86.6 %
Date: 2021-03-22 Branches: 869 2061 42.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_database_sygus.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 Implementation of term database sygus class
13
 **/
14
15
#include "theory/quantifiers/sygus/term_database_sygus.h"
16
17
#include "base/check.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/sygus_datatype.h"
20
#include "options/base_options.h"
21
#include "options/datatypes_options.h"
22
#include "options/quantifiers_options.h"
23
#include "printer/printer.h"
24
#include "theory/datatypes/sygus_datatype_utils.h"
25
#include "theory/quantifiers/quantifiers_attributes.h"
26
#include "theory/quantifiers/quantifiers_inference_manager.h"
27
#include "theory/quantifiers/quantifiers_state.h"
28
#include "theory/quantifiers/term_util.h"
29
#include "theory/rewriter.h"
30
31
using namespace CVC4::kind;
32
33
namespace CVC4 {
34
namespace theory {
35
namespace quantifiers {
36
37
std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
38
{
39
  switch (r)
40
  {
41
    case ROLE_ENUM_POOL: os << "POOL"; break;
42
    case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
43
    case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
44
    case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
45
    default: os << "enum_" << static_cast<unsigned>(r); break;
46
  }
47
  return os;
48
}
49
50
2190
TermDbSygus::TermDbSygus(QuantifiersState& qs)
51
    : d_qstate(qs),
52
2190
      d_syexp(new SygusExplain(this)),
53
2190
      d_ext_rw(new ExtendedRewriter(true)),
54
2190
      d_eval(new Evaluator),
55
2190
      d_funDefEval(new FunDefEvaluator),
56
10950
      d_eval_unfold(new SygusEvalUnfold(this))
57
{
58
2190
  d_true = NodeManager::currentNM()->mkConst( true );
59
2190
  d_false = NodeManager::currentNM()->mkConst( false );
60
2190
}
61
62
2190
void TermDbSygus::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; }
63
64
bool TermDbSygus::reset( Theory::Effort e ) {
65
  return true;
66
}
67
68
205332
TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
69
205332
  unsigned sindex = 0;
70
410664
  TypeNode vtn = tn;
71
410664
  TypeNode builtinType = tn;
72
205332
  if (tn.isDatatype())
73
  {
74
200958
    const DType& dt = tn.getDType();
75
200958
    if (!dt.getSygusType().isNull())
76
    {
77
200958
      builtinType = dt.getSygusType();
78
200958
      if (useSygusType)
79
      {
80
22149
        vtn = builtinType;
81
22149
        sindex = 1;
82
      }
83
    }
84
  }
85
205332
  NodeManager* nm = NodeManager::currentNM();
86
227708
  while( i>=(int)d_fv[sindex][tn].size() ){
87
22376
    std::stringstream ss;
88
11188
    if( tn.isDatatype() ){
89
5983
      const DType& dt = tn.getDType();
90
5983
      ss << "fv_" << dt.getName() << "_" << i;
91
    }else{
92
5205
      ss << "fv_" << tn << "_" << i;
93
    }
94
11188
    Assert(!vtn.isNull());
95
22376
    Node v = nm->mkBoundVar(ss.str(), vtn);
96
    // store its id, which is unique per builtin type, regardless of how it is
97
    // otherwise cached.
98
11188
    d_fvId[v] = d_fvTypeIdCounter[builtinType];
99
11188
    d_fvTypeIdCounter[builtinType]++;
100
22376
    Trace("sygus-db-debug") << "Free variable id " << v << " = " << d_fvId[v]
101
11188
                            << ", " << builtinType << std::endl;
102
11188
    d_fv[sindex][tn].push_back( v );
103
  }
104
410664
  return d_fv[sindex][tn][i];
105
}
106
107
103885
TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType ) {
108
103885
  std::map< TypeNode, int >::iterator it = var_count.find( tn );
109
103885
  if( it==var_count.end() ){
110
39724
    var_count[tn] = 1;
111
39724
    return getFreeVar( tn, 0, useSygusType );
112
  }else{
113
64161
    int index = it->second;
114
64161
    var_count[tn]++;
115
64161
    return getFreeVar( tn, index, useSygusType );
116
  }
117
}
118
119
4260
bool TermDbSygus::isFreeVar(Node n) const
120
{
121
4260
  return d_fvId.find(n) != d_fvId.end();
122
}
123
4196
size_t TermDbSygus::getFreeVarId(Node n) const
124
{
125
4196
  std::map<Node, size_t>::const_iterator it = d_fvId.find(n);
126
4196
  if (it == d_fvId.end())
127
  {
128
    Assert(false) << "TermDbSygus::isFreeVar: " << n
129
                  << " is not a cached free variable.";
130
    return 0;
131
  }
132
4196
  return it->second;
133
}
134
135
18
bool TermDbSygus::hasFreeVar( Node n, std::map< Node, bool >& visited ){
136
18
  if( visited.find( n )==visited.end() ){
137
18
    visited[n] = true;
138
18
    if( isFreeVar( n ) ){
139
18
      return true;
140
    }
141
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
142
      if( hasFreeVar( n[i], visited ) ){
143
        return true;
144
      }
145
    }
146
  }
147
  return false;
148
}
149
150
18
bool TermDbSygus::hasFreeVar( Node n ) {
151
36
  std::map< Node, bool > visited;
152
36
  return hasFreeVar( n, visited );
153
}
154
155
34
Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
156
{
157
34
  Assert(tn.isDatatype());
158
34
  Assert(tn.getDType().isSygus());
159
34
  Assert(tn.getDType().getSygusType().isComparableTo(c.getType()));
160
161
34
  std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
162
34
  if (it == d_proxy_vars[tn].end())
163
  {
164
29
    SygusTypeInfo& ti = getTypeInfo(tn);
165
29
    int anyC = ti.getAnyConstantConsNum();
166
58
    Node k;
167
29
    if (anyC == -1)
168
    {
169
      k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
170
      SygusPrintProxyAttribute spa;
171
      k.setAttribute(spa, c);
172
    }
173
    else
174
    {
175
29
      const DType& dt = tn.getDType();
176
87
      k = NodeManager::currentNM()->mkNode(
177
58
          APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
178
    }
179
29
    d_proxy_vars[tn][c] = k;
180
29
    return k;
181
  }
182
5
  return it->second;
183
}
184
185
616389
Node TermDbSygus::mkGeneric(const DType& dt,
186
                            unsigned c,
187
                            std::map<TypeNode, int>& var_count,
188
                            std::map<int, Node>& pre,
189
                            bool doBetaRed)
190
{
191
616389
  Assert(c < dt.getNumConstructors());
192
616389
  Assert(dt.isSygus());
193
616389
  Assert(!dt[c].getSygusOp().isNull());
194
1232778
  std::vector< Node > children;
195
1232778
  Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
196
616389
                          << std::endl;
197
1448779
  for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
198
  {
199
1664780
    Node a;
200
832390
    std::map< int, Node >::iterator it = pre.find( i );
201
832390
    if( it!=pre.end() ){
202
812015
      a = it->second;
203
812015
      Trace("sygus-db-debug") << "From pre: " << a << std::endl;
204
    }else{
205
40750
      TypeNode tna = dt[c].getArgType(i);
206
20375
      a = getFreeVarInc( tna, var_count, true );
207
    }
208
1664780
    Trace("sygus-db-debug")
209
832390
        << "  child " << i << " : " << a << " : " << a.getType() << std::endl;
210
832390
    Assert(!a.isNull());
211
832390
    children.push_back( a );
212
  }
213
616389
  Node ret = datatypes::utils::mkSygusTerm(dt, c, children, doBetaRed);
214
616389
  Trace("sygus-db-debug") << "mkGeneric returns " << ret << std::endl;
215
1232778
  return ret;
216
}
217
218
616389
Node TermDbSygus::mkGeneric(const DType& dt,
219
                            int c,
220
                            std::map<int, Node>& pre,
221
                            bool doBetaRed)
222
{
223
1232778
  std::map<TypeNode, int> var_count;
224
1232778
  return mkGeneric(dt, c, var_count, pre, doBetaRed);
225
}
226
227
15327
Node TermDbSygus::mkGeneric(const DType& dt, int c, bool doBetaRed)
228
{
229
30654
  std::map<int, Node> pre;
230
30654
  return mkGeneric(dt, c, pre, doBetaRed);
231
}
232
233
struct CanonizeBuiltinAttributeId
234
{
235
};
236
using CanonizeBuiltinAttribute =
237
    expr::Attribute<CanonizeBuiltinAttributeId, Node>;
238
239
Node TermDbSygus::canonizeBuiltin(Node n)
240
{
241
  std::map<TypeNode, int> var_count;
242
  return canonizeBuiltin(n, var_count);
243
}
244
245
68036
Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
246
{
247
  // has it already been computed?
248
68036
  if (var_count.empty() && n.hasAttribute(CanonizeBuiltinAttribute()))
249
  {
250
110996
    Node ret = n.getAttribute(CanonizeBuiltinAttribute());
251
55498
    Trace("sygus-db-canon") << "cached " << n << " : " << ret << "\n";
252
55498
    return ret;
253
  }
254
12538
  Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n << "\n";
255
25076
  Node ret = n;
256
  // it is symbolic if it represents "any constant"
257
12538
  if (n.getKind() == APPLY_SELECTOR_TOTAL)
258
  {
259
1838
    ret = getFreeVarInc(n[0].getType(), var_count, true);
260
  }
261
10700
  else if (n.getKind() != APPLY_CONSTRUCTOR)
262
  {
263
    ret = n;
264
  }
265
  else
266
  {
267
10700
    Assert(n.getKind() == APPLY_CONSTRUCTOR);
268
10700
    bool childChanged = false;
269
21400
    std::vector<Node> children;
270
10700
    children.push_back(n.getOperator());
271
27243
    for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j)
272
    {
273
33086
      Node child = canonizeBuiltin(n[j], var_count);
274
16543
      children.push_back(child);
275
16543
      childChanged = childChanged || child != n[j];
276
    }
277
10700
    if (childChanged)
278
    {
279
2653
      ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
280
    }
281
  }
282
  // cache if we had a fresh variable count
283
12538
  if (var_count.empty())
284
  {
285
7815
    n.setAttribute(CanonizeBuiltinAttribute(), ret);
286
  }
287
25076
  Trace("sygus-db-canon") << "  ...normalized " << n << " --> " << ret
288
12538
                          << std::endl;
289
12538
  Assert(ret.getType().isComparableTo(n.getType()));
290
12538
  return ret;
291
}
292
293
struct SygusToBuiltinAttributeId
294
{
295
};
296
typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
297
    SygusToBuiltinAttribute;
298
299
267138
Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
300
{
301
267138
  if (n.isConst())
302
  {
303
    // if its a constant, we use the datatype utility version
304
248401
    return datatypes::utils::sygusToBuiltin(n);
305
  }
306
18737
  Assert(n.getType().isComparableTo(tn));
307
18737
  if (!tn.isDatatype())
308
  {
309
167
    return n;
310
  }
311
  // has it already been computed?
312
18570
  if (n.hasAttribute(SygusToBuiltinAttribute()))
313
  {
314
6954
    return n.getAttribute(SygusToBuiltinAttribute());
315
  }
316
23232
  Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
317
11616
                          << ", type = " << tn << std::endl;
318
11616
  const DType& dt = tn.getDType();
319
11616
  if (!dt.isSygus())
320
  {
321
    return n;
322
  }
323
11616
  if (n.getKind() == APPLY_CONSTRUCTOR)
324
  {
325
7424
    unsigned i = datatypes::utils::indexOf(n.getOperator());
326
7424
    Assert(n.getNumChildren() == dt[i].getNumArgs());
327
14848
    std::map<int, Node> pre;
328
22886
    for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
329
    {
330
15462
      pre[j] = sygusToBuiltin(n[j], dt[i].getArgType(j));
331
30924
      Trace("sygus-db-debug")
332
15462
          << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
333
    }
334
14848
    Node ret = mkGeneric(dt, i, pre);
335
14848
    Trace("sygus-db-debug")
336
7424
        << "SygusToBuiltin : Generic is " << ret << std::endl;
337
    // cache
338
7424
    n.setAttribute(SygusToBuiltinAttribute(), ret);
339
7424
    return ret;
340
  }
341
4192
  if (n.hasAttribute(SygusPrintProxyAttribute()))
342
  {
343
    // this variable was associated by an attribute to a builtin node
344
    return n.getAttribute(SygusPrintProxyAttribute());
345
  }
346
4192
  Assert(isFreeVar(n));
347
  // map to builtin variable type
348
4192
  size_t fv_num = getFreeVarId(n);
349
4192
  Assert(!dt.getSygusType().isNull());
350
8384
  TypeNode vtn = dt.getSygusType();
351
8384
  Node ret = getFreeVar(vtn, fv_num);
352
8384
  Trace("sygus-db-debug") << "SygusToBuiltin: variable for " << n << " is "
353
4192
                          << ret << ", fv_num=" << fv_num << std::endl;
354
4192
  return ret;
355
}
356
357
350589
unsigned TermDbSygus::getSygusTermSize( Node n ){
358
350589
  if (n.getKind() != APPLY_CONSTRUCTOR)
359
  {
360
1866
    return 0;
361
  }
362
348723
  unsigned sum = 0;
363
564372
  for (unsigned i = 0; i < n.getNumChildren(); i++)
364
  {
365
215649
    sum += getSygusTermSize(n[i]);
366
  }
367
348723
  const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
368
348723
  int cindex = datatypes::utils::indexOf(n.getOperator());
369
348723
  Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
370
348723
  unsigned weight = dt[cindex].getWeight();
371
348723
  return weight + sum;
372
}
373
374
19021
bool TermDbSygus::registerSygusType(TypeNode tn)
375
{
376
19021
  std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn);
377
19021
  if (it != d_registerStatus.end())
378
  {
379
    // already registered
380
16284
    return it->second;
381
  }
382
2737
  d_registerStatus[tn] = false;
383
  // it must be a sygus datatype
384
2737
  if (!tn.isDatatype())
385
  {
386
55
    return false;
387
  }
388
2682
  const DType& dt = tn.getDType();
389
2682
  if (!dt.isSygus())
390
  {
391
    return false;
392
  }
393
2682
  d_registerStatus[tn] = true;
394
2682
  SygusTypeInfo& sti = d_tinfo[tn];
395
2682
  sti.initialize(this, tn);
396
2682
  return true;
397
}
398
399
657
void TermDbSygus::registerEnumerator(Node e,
400
                                     Node f,
401
                                     SynthConjecture* conj,
402
                                     EnumeratorRole erole)
403
{
404
657
  if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
405
  {
406
    // already registered
407
    return;
408
  }
409
657
  Trace("sygus-db") << "Register enumerator : " << e << std::endl;
410
  // register its type
411
1314
  TypeNode et = e.getType();
412
657
  registerSygusType(et);
413
657
  d_enum_to_conjecture[e] = conj;
414
657
  d_enum_to_synth_fun[e] = f;
415
657
  NodeManager* nm = NodeManager::currentNM();
416
417
1314
  Trace("sygus-db") << "  registering symmetry breaking clauses..."
418
657
                    << std::endl;
419
  // depending on if we are using symbolic constructors, introduce symmetry
420
  // breaking lemma templates for each relevant subtype of the grammar
421
657
  SygusTypeInfo& eti = getTypeInfo(et);
422
1314
  std::vector<TypeNode> sf_types;
423
657
  eti.getSubfieldTypes(sf_types);
424
  // for each type of subfield type of this enumerator
425
2053
  for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
426
  {
427
2792
    std::vector<unsigned> rm_indices;
428
2792
    TypeNode stn = sf_types[i];
429
1396
    Assert(stn.isDatatype());
430
1396
    SygusTypeInfo& sti = getTypeInfo(stn);
431
1396
    const DType& dt = stn.getDType();
432
1396
    int anyC = sti.getAnyConstantConsNum();
433
9821
    for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
434
    {
435
8425
      bool isAnyC = static_cast<int>(j) == anyC;
436
8425
      if (anyC != -1 && !isAnyC)
437
      {
438
        // if we are using the any constant constructor, do not use any
439
        // concrete constant
440
562
        Node c_op = sti.getConsNumConst(j);
441
281
        if (!c_op.isNull())
442
        {
443
61
          rm_indices.push_back(j);
444
        }
445
      }
446
    }
447
1457
    for (unsigned& rindex : rm_indices)
448
    {
449
      // make the apply-constructor corresponding to an application of the
450
      // constant or "any constant" constructor
451
      // we call getInstCons since in the case of any constant constructors, it
452
      // is necessary to generate a term of the form any_constant( x.0 ) for a
453
      // fresh variable x.0.
454
122
      Node fv = getFreeVar(stn, 0);
455
122
      Node exc_val = datatypes::utils::getInstCons(fv, dt, rindex);
456
      // should not include the constuctor in any subterm
457
122
      Node x = getFreeVar(stn, 0);
458
122
      Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
459
61
                        << " == " << exc_val << std::endl;
460
122
      Node lem = getExplain()->getExplanationForEquality(x, exc_val);
461
61
      lem = lem.negate();
462
122
      Trace("cegqi-lemma")
463
61
          << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
464
61
          << std::endl;
465
      // the size of the subterm we are blocking is the weight of the
466
      // constructor (usually zero)
467
61
      registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
468
    }
469
  }
470
657
  Trace("sygus-db") << "  ...finished" << std::endl;
471
472
  // determine if we are actively-generated
473
657
  bool isActiveGen = false;
474
657
  if (options::sygusActiveGenMode() != options::SygusActiveGenMode::NONE)
475
  {
476
649
    if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
477
    {
478
      // If the enumerator is a solution for a conjecture with multiple
479
      // functions, we do not use active generation. If we did, we would have to
480
      // generate a "product" of two actively-generated enumerators. That is,
481
      // given a conjecture with two functions-to-synthesize with enumerators
482
      // e_f and e_g, and if these enumerators generated:
483
      // e_f -> t1, ..., tn
484
      // e_g -> s1, ..., sm
485
      // The sygus module in charge of this conjecture would expect
486
      // constructCandidates calls of the form
487
      //   (e_f,e_g) -> (ti, sj)
488
      // for each i,j. We instead use passive enumeration in this case.
489
      //
490
      // If the enumerator is constrained, it cannot be actively generated.
491
    }
492
348
    else if (erole == ROLE_ENUM_POOL)
493
    {
494
      // If the enumerator is used for generating a pool of values, we always
495
      // use active generation.
496
110
      isActiveGen = true;
497
    }
498
238
    else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
499
    {
500
      // If the enumerator is the single function-to-synthesize, if auto is
501
      // enabled, we infer whether it is better to enable active generation.
502
238
      if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO)
503
      {
504
        // We use active generation if the grammar of the enumerator does not
505
        // have ITE and is not Boolean. Experimentally, it is better to
506
        // use passive generation for these cases since it enables useful
507
        // search space pruning techniques, e.g. evaluation unfolding,
508
        // conjecture-specific symmetry breaking. Also, if sygus-stream is
509
        // enabled, we always use active generation, since the use cases of
510
        // sygus stream are to find many solutions to an easy problem, where
511
        // the bottleneck often becomes the large number of "exclude the current
512
        // solution" clauses.
513
226
        const DType& dt = et.getDType();
514
452
        if (options::sygusStream()
515
452
            || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
516
        {
517
77
          isActiveGen = true;
518
        }
519
      }
520
      else
521
      {
522
12
        isActiveGen = true;
523
      }
524
    }
525
    else
526
    {
527
      Unreachable() << "Unknown enumerator mode in registerEnumerator";
528
    }
529
  }
530
1314
  Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
531
657
                    << " returned " << isActiveGen << std::endl;
532
  // Currently, actively-generated enumerators are either basic or variable
533
  // agnostic.
534
  bool isVarAgnostic = isActiveGen
535
657
                       && options::sygusActiveGenMode()
536
657
                              == options::SygusActiveGenMode::VAR_AGNOSTIC;
537
657
  d_enum_var_agnostic[e] = isVarAgnostic;
538
657
  if (isVarAgnostic)
539
  {
540
    // requires variable subclasses
541
2
    eti.initializeVarSubclasses();
542
    // If no subclass has more than one variable, do not use variable agnostic
543
    // enumeration
544
2
    bool useVarAgnostic = !eti.isSubclassVarTrivial();
545
2
    if (!useVarAgnostic)
546
    {
547
      Trace("sygus-db")
548
          << "...disabling variable agnostic for " << e
549
          << " since it has no subclass with more than one variable."
550
          << std::endl;
551
      d_enum_var_agnostic[e] = false;
552
      isActiveGen = false;
553
    }
554
  }
555
657
  d_enum_active_gen[e] = isActiveGen;
556
657
  d_enum_basic[e] = isActiveGen && !isVarAgnostic;
557
558
  // We make an active guard if we will be explicitly blocking solutions for
559
  // the enumerator. This is the case if the role of the enumerator is to
560
  // populate a pool of terms, or (some cases) of when it is actively generated.
561
657
  if (isActiveGen || erole == ROLE_ENUM_POOL)
562
  {
563
    // make the guard
564
406
    Node ag = nm->mkSkolem("eG", nm->booleanType());
565
    // must ensure it is a literal immediately here
566
203
    ag = d_qstate.getValuation().ensureLiteral(ag);
567
    // must ensure that it is asserted as a literal before we begin solving
568
406
    Node lem = nm->mkNode(OR, ag, ag.negate());
569
203
    d_qim->requirePhase(ag, true);
570
203
    d_qim->lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT);
571
203
    d_enum_to_active_guard[e] = ag;
572
  }
573
}
574
575
90922
bool TermDbSygus::isEnumerator(Node e) const
576
{
577
90922
  return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
578
}
579
580
629
SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
581
{
582
  std::map<Node, SynthConjecture*>::const_iterator itm =
583
629
      d_enum_to_conjecture.find(e);
584
629
  if (itm != d_enum_to_conjecture.end()) {
585
629
    return itm->second;
586
  }
587
  return nullptr;
588
}
589
590
508
Node TermDbSygus::getSynthFunForEnumerator(Node e) const
591
{
592
508
  std::map<Node, Node>::const_iterator itsf = d_enum_to_synth_fun.find(e);
593
508
  if (itsf != d_enum_to_synth_fun.end())
594
  {
595
508
    return itsf->second;
596
  }
597
  return Node::null();
598
}
599
600
87958
Node TermDbSygus::getActiveGuardForEnumerator(Node e) const
601
{
602
87958
  std::map<Node, Node>::const_iterator itag = d_enum_to_active_guard.find(e);
603
87958
  if (itag != d_enum_to_active_guard.end()) {
604
49702
    return itag->second;
605
  }
606
38256
  return Node::null();
607
}
608
609
9518
bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
610
{
611
9518
  std::map<Node, bool>::const_iterator itus = d_enum_to_using_sym_cons.find(e);
612
9518
  if (itus != d_enum_to_using_sym_cons.end())
613
  {
614
    return itus->second;
615
  }
616
9518
  return false;
617
}
618
619
28857
bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
620
{
621
28857
  std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e);
622
28857
  if (itus != d_enum_var_agnostic.end())
623
  {
624
28857
    return itus->second;
625
  }
626
  return false;
627
}
628
629
431
bool TermDbSygus::isBasicEnumerator(Node e) const
630
{
631
431
  std::map<Node, bool>::const_iterator itus = d_enum_basic.find(e);
632
431
  if (itus != d_enum_basic.end())
633
  {
634
431
    return itus->second;
635
  }
636
  return false;
637
}
638
639
104977
bool TermDbSygus::isPassiveEnumerator(Node e) const
640
{
641
104977
  std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e);
642
104977
  if (itus != d_enum_active_gen.end())
643
  {
644
84205
    return !itus->second;
645
  }
646
20772
  return true;
647
}
648
649
9991
void TermDbSygus::getEnumerators(std::vector<Node>& mts)
650
{
651
19251
  for (std::map<Node, SynthConjecture*>::iterator itm =
652
9991
           d_enum_to_conjecture.begin();
653
29242
       itm != d_enum_to_conjecture.end();
654
       ++itm)
655
  {
656
19251
    mts.push_back( itm->first );
657
  }
658
9991
}
659
660
124
void TermDbSygus::registerSymBreakLemma(
661
    Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl)
662
{
663
124
  d_enum_to_sb_lemmas[e].push_back(lem);
664
124
  d_sb_lemma_to_type[lem] = tn;
665
124
  d_sb_lemma_to_size[lem] = sz;
666
124
  d_sb_lemma_to_isTempl[lem] = isTempl;
667
124
}
668
669
9991
bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const
670
{
671
9991
  if (!d_enum_to_sb_lemmas.empty())
672
  {
673
611
    for (std::pair<const Node, std::vector<Node> > sb : d_enum_to_sb_lemmas)
674
    {
675
316
      enums.push_back(sb.first);
676
    }
677
295
    return true;
678
  }
679
9696
  return false;
680
}
681
682
199
void TermDbSygus::getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const
683
{
684
  std::map<Node, std::vector<Node> >::const_iterator itsb =
685
199
      d_enum_to_sb_lemmas.find(e);
686
199
  if (itsb != d_enum_to_sb_lemmas.end())
687
  {
688
86
    lemmas.insert(lemmas.end(), itsb->second.begin(), itsb->second.end());
689
  }
690
199
}
691
692
14
TypeNode TermDbSygus::getTypeForSymBreakLemma(Node lem) const
693
{
694
14
  std::map<Node, TypeNode>::const_iterator it = d_sb_lemma_to_type.find(lem);
695
14
  Assert(it != d_sb_lemma_to_type.end());
696
14
  return it->second;
697
}
698
14
unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
699
{
700
14
  std::map<Node, unsigned>::const_iterator it = d_sb_lemma_to_size.find(lem);
701
14
  Assert(it != d_sb_lemma_to_size.end());
702
14
  return it->second;
703
}
704
705
124
bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const
706
{
707
124
  std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem);
708
124
  Assert(it != d_sb_lemma_to_isTempl.end());
709
124
  return it->second;
710
}
711
712
6
void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
713
714
206198
bool TermDbSygus::isRegistered(TypeNode tn) const
715
{
716
206198
  return d_tinfo.find(tn) != d_tinfo.end();
717
}
718
719
11315
TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
720
11315
  std::map<TypeNode, SygusTypeInfo>::iterator it = d_tinfo.find(tn);
721
11315
  Assert(it != d_tinfo.end());
722
11315
  return it->second.getBuiltinType();
723
}
724
725
16401
void TermDbSygus::toStreamSygus(const char* c, Node n)
726
{
727
16401
  if (Trace.isOn(c))
728
  {
729
    std::stringstream ss;
730
    toStreamSygus(ss, n);
731
    Trace(c) << ss.str();
732
  }
733
16401
}
734
735
300
void TermDbSygus::toStreamSygus(std::ostream& out, Node n)
736
{
737
300
  if (n.isNull())
738
  {
739
    out << n;
740
    return;
741
  }
742
  // use external conversion
743
300
  out << datatypes::utils::sygusToBuiltin(n, true);
744
}
745
746
304693
SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
747
{
748
304693
  AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
749
304693
  return d_tinfo[tn];
750
}
751
752
576207
Node TermDbSygus::rewriteNode(Node n) const
753
{
754
1152414
  Node res = Rewriter::rewrite(n);
755
576207
  if (res.isConst())
756
  {
757
    // constant, we are done
758
327676
    return res;
759
  }
760
248531
  if (options::sygusRecFun())
761
  {
762
223393
    if (d_funDefEval->hasDefinitions())
763
    {
764
      // If recursive functions are enabled, then we use the recursive function
765
      // evaluation utility.
766
4603
      Node fres = d_funDefEval->evaluate(res);
767
3664
      if (!fres.isNull())
768
      {
769
2725
        return fres;
770
      }
771
      // It may have failed, in which case there are undefined symbols in res or
772
      // we reached the limit of evaluations. In this case, we revert to the
773
      // result of rewriting in the return statement below.
774
    }
775
  }
776
245806
  return res;
777
}
778
779
1775
unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
780
{
781
  std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
782
1775
      d_sel_weight.find(tn);
783
1775
  if (itsw == d_sel_weight.end())
784
  {
785
348
    d_sel_weight[tn].clear();
786
348
    itsw = d_sel_weight.find(tn);
787
348
    const DType& dt = tn.getDType();
788
696
    Trace("sygus-db") << "Compute selector weights for " << dt.getName()
789
348
                      << std::endl;
790
1982
    for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
791
    {
792
1634
      unsigned cw = dt[i].getWeight();
793
3593
      for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
794
      {
795
3918
        Node csel = dt[i].getSelectorInternal(tn, j);
796
1959
        std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
797
1959
        if (its == itsw->second.end() || cw < its->second)
798
        {
799
1033
          d_sel_weight[tn][csel] = cw;
800
1033
          Trace("sygus-db") << "  w(" << csel << ") <= " << cw << std::endl;
801
        }
802
      }
803
    }
804
  }
805
1775
  Assert(itsw->second.find(sel) != itsw->second.end());
806
1775
  return itsw->second[sel];
807
}
808
809
655116
TypeNode TermDbSygus::getArgType(const DTypeConstructor& c, unsigned i) const
810
{
811
655116
  Assert(i < c.getNumArgs());
812
655116
  return c.getArgType(i);
813
}
814
815
8
bool TermDbSygus::isTypeMatch(const DTypeConstructor& c1,
816
                              const DTypeConstructor& c2)
817
{
818
8
  if( c1.getNumArgs()!=c2.getNumArgs() ){
819
    return false;
820
  }else{
821
24
    for( unsigned i=0; i<c1.getNumArgs(); i++ ){
822
16
      if( getArgType( c1, i )!=getArgType( c2, i ) ){
823
        return false;
824
      }
825
    }
826
8
    return true;
827
  }
828
}
829
830
bool TermDbSygus::isSymbolicConsApp(Node n) const
831
{
832
  if (n.getKind() != APPLY_CONSTRUCTOR)
833
  {
834
    return false;
835
  }
836
  TypeNode tn = n.getType();
837
  Assert(tn.isDatatype());
838
  const DType& dt = tn.getDType();
839
  Assert(dt.isSygus());
840
  unsigned cindex = datatypes::utils::indexOf(n.getOperator());
841
  Node sygusOp = dt[cindex].getSygusOp();
842
  // it is symbolic if it represents "any constant"
843
  return sygusOp.getAttribute(SygusAnyConstAttribute());
844
}
845
846
3699
bool TermDbSygus::canConstructKind(TypeNode tn,
847
                                   Kind k,
848
                                   std::vector<TypeNode>& argts,
849
                                   bool aggr)
850
{
851
3699
  Assert(isRegistered(tn));
852
3699
  SygusTypeInfo& ti = getTypeInfo(tn);
853
3699
  int c = ti.getKindConsNum(k);
854
3699
  const DType& dt = tn.getDType();
855
3699
  if (c != -1)
856
  {
857
10274
    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
858
    {
859
6876
      argts.push_back(dt[c].getArgType(i));
860
    }
861
3398
    return true;
862
  }
863
602
  if (!options::sygusSymBreakAgg())
864
  {
865
    return false;
866
  }
867
301
  if (sygusToBuiltinType(tn).isBoolean())
868
  {
869
295
    if (k == ITE)
870
    {
871
      // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) )
872
256
      std::vector<TypeNode> conj_types;
873
224
      if (canConstructKind(tn, AND, conj_types, true) && conj_types.size() == 2)
874
      {
875
200
        bool success = true;
876
600
        std::vector<TypeNode> disj_types[2];
877
584
        for (unsigned cc = 0; cc < 2; cc++)
878
        {
879
1176
          if (!canConstructKind(conj_types[cc], OR, disj_types[cc], true)
880
1176
              || disj_types[cc].size() != 2)
881
          {
882
8
            success = false;
883
8
            break;
884
          }
885
        }
886
200
        if (success)
887
        {
888
192
          for (unsigned r = 0; r < 2; r++)
889
          {
890
192
            for (unsigned d = 0, size = disj_types[r].size(); d < size; d++)
891
            {
892
192
              TypeNode dtn = disj_types[r][d];
893
              // must have negation that occurs in the other conjunct
894
192
              std::vector<TypeNode> ntypes;
895
192
              if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1)
896
              {
897
192
                TypeNode ntn = ntypes[0];
898
192
                for (unsigned dd = 0, inner_size = disj_types[1 - r].size();
899
192
                     dd < inner_size;
900
                     dd++)
901
                {
902
192
                  if (disj_types[1 - r][dd] == ntn)
903
                  {
904
192
                    argts.push_back(ntn);
905
192
                    argts.push_back(disj_types[r][d]);
906
192
                    argts.push_back(disj_types[1 - r][1 - dd]);
907
192
                    if (Trace.isOn("sygus-cons-kind"))
908
                    {
909
                      Trace("sygus-cons-kind")
910
                          << "Can construct kind " << k << " in " << tn
911
                          << " via child types:" << std::endl;
912
                      for (unsigned i = 0; i < 3; i++)
913
                      {
914
                        Trace("sygus-cons-kind")
915
                            << "  " << argts[i] << std::endl;
916
                      }
917
                    }
918
192
                    return true;
919
                  }
920
                }
921
              }
922
            }
923
          }
924
        }
925
      }
926
    }
927
  }
928
  // could try aggressive inferences here, such as
929
  // (and b1 b2) <---- (not (or (not b1) (not b2)))
930
  // (or b1 b2)  <---- (not (and (not b1) (not b2)))
931
109
  return false;
932
}
933
934
29327
bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
935
29327
  if( visited.find( n )==visited.end() ){
936
27664
    visited[n] = true;
937
27664
    Kind k = n.getKind();
938
27664
    if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL ||
939
27558
        k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
940
124
      if( n[1].isConst() ){
941
106
        if (n[1] == TermUtil::mkTypeValue(n[1].getType(), 0))
942
        {
943
          return true;
944
        }
945
      }else{
946
        // if it has free variables it might be a non-zero constant
947
18
        if( !hasFreeVar( n[1] ) ){
948
          return true;
949
        }
950
      }
951
    }
952
48675
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
953
21011
      if( involvesDivByZero( n[i], visited ) ){
954
        return true;
955
      }
956
    }
957
  }
958
29327
  return false;
959
}
960
961
8316
bool TermDbSygus::involvesDivByZero( Node n ) {
962
16632
  std::map< Node, bool > visited;
963
16632
  return involvesDivByZero( n, visited );
964
}
965
966
3714
Node TermDbSygus::getAnchor( Node n ) {
967
3714
  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
968
1652
    return getAnchor( n[0] );
969
  }else{
970
2062
    return n;
971
  }
972
}
973
974
unsigned TermDbSygus::getAnchorDepth( Node n ) {
975
  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
976
    return 1+getAnchorDepth( n[0] );
977
  }else{
978
    return 0;
979
  }
980
}
981
982
196865
Node TermDbSygus::evaluateBuiltin(TypeNode tn,
983
                                  Node bn,
984
                                  const std::vector<Node>& args,
985
                                  bool tryEval)
986
{
987
196865
  if (args.empty())
988
  {
989
615
    return Rewriter::rewrite( bn );
990
  }
991
196250
  Assert(isRegistered(tn));
992
196250
  SygusTypeInfo& ti = getTypeInfo(tn);
993
196250
  const std::vector<Node>& varlist = ti.getVarList();
994
196250
  Assert(varlist.size() == args.size());
995
996
392500
  Node res;
997
392500
  if (tryEval && options::sygusEvalOpt())
998
  {
999
    // Try evaluating, which is much faster than substitution+rewriting.
1000
    // This may fail if there is a subterm of bn under the
1001
    // substitution that is not constant, or if an operator in bn is not
1002
    // supported by the evaluator
1003
196250
    res = d_eval->eval(bn, varlist, args);
1004
  }
1005
196250
  if (res.isNull())
1006
  {
1007
    // must do substitution
1008
    res =
1009
        bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
1010
  }
1011
  // Call the rewrite node function, which may involve recursive function
1012
  // evaluation.
1013
196250
  return rewriteNode(res);
1014
}
1015
1016
808603
Node TermDbSygus::evaluateWithUnfolding(
1017
    Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited)
1018
{
1019
  std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
1020
808603
      visited.find(n);
1021
808603
  if( it==visited.end() ){
1022
1019270
    Node ret = n;
1023
749765
    while (ret.getKind() == DT_SYGUS_EVAL
1024
1259400
           && ret[0].getKind() == APPLY_CONSTRUCTOR)
1025
    {
1026
120065
      if (ret == n && ret[0].isConst())
1027
      {
1028
        // use rewriting, possibly involving recursive functions
1029
55479
        ret = rewriteNode(ret);
1030
      }
1031
      else
1032
      {
1033
64586
        ret = d_eval_unfold->unfold(ret);
1034
      }
1035
    }
1036
509635
    if( ret.getNumChildren()>0 ){
1037
642588
      std::vector< Node > children;
1038
321294
      if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){
1039
34909
        children.push_back( ret.getOperator() );
1040
      }
1041
321294
      bool childChanged = false;
1042
1015865
      for( unsigned i=0; i<ret.getNumChildren(); i++ ){
1043
1389142
        Node nc = evaluateWithUnfolding(ret[i], visited);
1044
694571
        childChanged = childChanged || nc!=ret[i];
1045
694571
        children.push_back( nc );
1046
      }
1047
321294
      if( childChanged ){
1048
139245
        ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
1049
      }
1050
321294
      if (options::sygusExtRew())
1051
      {
1052
310022
        ret = getExtRewriter()->extendedRewrite(ret);
1053
      }
1054
      // use rewriting, possibly involving recursive functions
1055
321294
      ret = rewriteNode(ret);
1056
    }
1057
509635
    visited[n] = ret;
1058
509635
    return ret;
1059
  }else{
1060
298968
    return it->second;
1061
  }
1062
}
1063
1064
11639
Node TermDbSygus::evaluateWithUnfolding(Node n)
1065
{
1066
23278
  std::unordered_map<Node, Node, NodeHashFunction> visited;
1067
23278
  return evaluateWithUnfolding(n, visited);
1068
}
1069
1070
842
bool TermDbSygus::isEvaluationPoint(Node n) const
1071
{
1072
842
  if (n.getKind() != DT_SYGUS_EVAL)
1073
  {
1074
527
    return false;
1075
  }
1076
315
  if (!n[0].isVar())
1077
  {
1078
    return false;
1079
  }
1080
1488
  for (unsigned i = 1, nchild = n.getNumChildren(); i < nchild; i++)
1081
  {
1082
1173
    if (!n[i].isConst())
1083
    {
1084
      return false;
1085
    }
1086
  }
1087
315
  return true;
1088
}
1089
1090
}/* CVC4::theory::quantifiers namespace */
1091
}/* CVC4::theory namespace */
1092
223227
}/* CVC4 namespace */