GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sort_inference.cpp Lines: 437 519 84.2 %
Date: 2021-03-23 Branches: 1016 2224 45.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sort_inference.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Paul Meng, 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 Sort inference module
13
 **
14
 ** This class implements sort inference, based on a simple algorithm:
15
 ** First, we assume all functions and predicates have distinct uninterpreted
16
 ** types.
17
 ** One pass is made through the input assertions, while a union-find data
18
 ** structure maintains necessary information regarding constraints on these
19
 ** types.
20
 **/
21
22
#include "theory/sort_inference.h"
23
24
#include <vector>
25
26
#include "options/quantifiers_options.h"
27
#include "options/smt_options.h"
28
#include "options/uf_options.h"
29
#include "theory/rewriter.h"
30
#include "theory/quantifiers/quant_util.h"
31
32
using namespace CVC4;
33
using namespace CVC4::kind;
34
using namespace std;
35
36
namespace CVC4 {
37
namespace theory {
38
39
void SortInference::UnionFind::print(const char * c){
40
  for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){
41
    Trace(c) << "s_" << it->first << " = s_" << it->second << ", ";
42
  }
43
  for( unsigned i=0; i<d_deq.size(); i++ ){
44
    Trace(c) << "s_" << d_deq[i].first << " != s_" << d_deq[i].second << ", ";
45
  }
46
  Trace(c) << std::endl;
47
}
48
void SortInference::UnionFind::set( UnionFind& c ) {
49
  clear();
50
  for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){
51
    d_eqc[ it->first ] = it->second;
52
  }
53
  d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() );
54
}
55
1254
int SortInference::UnionFind::getRepresentative( int t ){
56
1254
  std::map< int, int >::iterator it = d_eqc.find( t );
57
1254
  if( it==d_eqc.end() || it->second==t ){
58
891
    return t;
59
  }else{
60
363
    int rt = getRepresentative( it->second );
61
363
    d_eqc[t] = rt;
62
363
    return rt;
63
  }
64
}
65
void SortInference::UnionFind::setEqual( int t1, int t2 ){
66
  if( t1!=t2 ){
67
    int rt1 = getRepresentative( t1 );
68
    int rt2 = getRepresentative( t2 );
69
    if( rt1>rt2 ){
70
      d_eqc[rt1] = rt2;
71
    }else{
72
      d_eqc[rt2] = rt1;
73
    }
74
  }
75
}
76
bool SortInference::UnionFind::isValid() {
77
  for( unsigned i=0; i<d_deq.size(); i++ ){
78
    if( areEqual( d_deq[i].first, d_deq[i].second ) ){
79
      return false;
80
    }
81
  }
82
  return true;
83
}
84
85
86
55
void SortInference::recordSubsort( TypeNode tn, int s ){
87
55
  s = d_type_union_find.getRepresentative( s );
88
55
  if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){
89
16
    d_sub_sorts.push_back( s );
90
16
    d_type_sub_sorts[tn].push_back( s );
91
  }
92
55
}
93
94
400
void SortInference::printSort( const char* c, int t ){
95
400
  int rt = d_type_union_find.getRepresentative( t );
96
400
  if( d_type_types.find( rt )!=d_type_types.end() ){
97
174
    Trace(c) << d_type_types[rt];
98
  }else{
99
226
    Trace(c) << "s_" << rt;
100
  }
101
400
}
102
103
12
void SortInference::reset() {
104
12
  d_sub_sorts.clear();
105
12
  d_non_monotonic_sorts.clear();
106
12
  d_type_sub_sorts.clear();
107
  //reset info
108
12
  d_sortCount = 1;
109
12
  d_type_union_find.clear();
110
12
  d_type_types.clear();
111
12
  d_id_for_types.clear();
112
12
  d_op_return_types.clear();
113
12
  d_op_arg_types.clear();
114
12
  d_var_types.clear();
115
  //for rewriting
116
12
  d_symbol_map.clear();
117
12
  d_const_map.clear();
118
12
}
119
120
12
void SortInference::initialize(const std::vector<Node>& assertions)
121
{
122
12
  Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl;
123
  // process all assertions
124
24
  std::map<Node, int> visited;
125
12
  NodeManager * nm = NodeManager::currentNM();
126
12
  int btId = getIdForType( nm->booleanType() );
127
61
  for (const Node& a : assertions)
128
  {
129
49
    Trace("sort-inference-debug") << "Process " << a << std::endl;
130
98
    std::map<Node, Node> var_bound;
131
49
    int pid = process(a, var_bound, visited);
132
    // the type of the topmost term must be Boolean
133
49
    setEqual( pid, btId );
134
  }
135
12
  Trace("sort-inference-proc") << "...done" << std::endl;
136
48
  for (const std::pair<const Node, int>& rt : d_op_return_types)
137
  {
138
36
    Trace("sort-inference") << rt.first << " : ";
139
72
    TypeNode retTn = rt.first.getType();
140
36
    if (!d_op_arg_types[rt.first].empty())
141
    {
142
7
      Trace("sort-inference") << "( ";
143
15
      for (size_t i = 0; i < d_op_arg_types[rt.first].size(); i++)
144
      {
145
8
        recordSubsort(retTn[i], d_op_arg_types[rt.first][i]);
146
8
        printSort("sort-inference", d_op_arg_types[rt.first][i]);
147
8
        Trace("sort-inference") << " ";
148
      }
149
7
      Trace("sort-inference") << ") -> ";
150
7
      retTn = retTn[(int)retTn.getNumChildren() - 1];
151
    }
152
36
    recordSubsort(retTn, rt.second);
153
36
    printSort("sort-inference", rt.second);
154
36
    Trace("sort-inference") << std::endl;
155
  }
156
18
  for (std::pair<const Node, std::map<Node, int> >& vt : d_var_types)
157
  {
158
12
    Trace("sort-inference")
159
6
        << "Quantified formula : " << vt.first << " : " << std::endl;
160
17
    for (const Node& v : vt.first[0])
161
    {
162
11
      recordSubsort(v.getType(), vt.second[v]);
163
11
      printSort("sort-inference", vt.second[v]);
164
11
      Trace("sort-inference") << std::endl;
165
    }
166
6
    Trace("sort-inference") << std::endl;
167
  }
168
169
  // determine monotonicity of sorts
170
24
  Trace("sort-inference-proc")
171
12
      << "Calculating monotonicty for subsorts..." << std::endl;
172
24
  std::map<Node, std::map<int, bool> > visitedm;
173
61
  for (const Node& a : assertions)
174
  {
175
98
    Trace("sort-inference-debug")
176
49
        << "Process monotonicity for " << a << std::endl;
177
98
    std::map<Node, Node> var_bound;
178
49
    processMonotonic(a, true, true, var_bound, visitedm);
179
  }
180
12
  Trace("sort-inference-proc") << "...done" << std::endl;
181
182
24
  Trace("sort-inference") << "We have " << d_sub_sorts.size()
183
12
                          << " sub-sorts : " << std::endl;
184
28
  for (unsigned i = 0, size = d_sub_sorts.size(); i < size; i++)
185
  {
186
16
    printSort("sort-inference", d_sub_sorts[i]);
187
16
    if (d_type_types.find(d_sub_sorts[i]) != d_type_types.end())
188
    {
189
11
      Trace("sort-inference") << " is interpreted." << std::endl;
190
    }
191
15
    else if (d_non_monotonic_sorts.find(d_sub_sorts[i])
192
15
             == d_non_monotonic_sorts.end())
193
    {
194
4
      Trace("sort-inference") << " is monotonic." << std::endl;
195
    }
196
    else
197
    {
198
1
      Trace("sort-inference") << " is not monotonic." << std::endl;
199
    }
200
  }
201
12
}
202
203
49
Node SortInference::simplify(Node n,
204
                             std::map<Node, Node>& model_replace_f,
205
                             std::map<Node, std::map<TypeNode, Node> >& visited)
206
{
207
49
  Trace("sort-inference-debug") << "Simplify " << n << std::endl;
208
98
  std::map<Node, Node> var_bound;
209
98
  TypeNode tnn;
210
49
  Node ret = simplifyNode(n, var_bound, tnn, model_replace_f, visited);
211
49
  ret = theory::Rewriter::rewrite(ret);
212
98
  return ret;
213
}
214
215
12
void SortInference::getNewAssertions(std::vector<Node>& new_asserts)
216
{
217
12
  NodeManager* nm = NodeManager::currentNM();
218
  // now, ensure constants are distinct
219
13
  for (const std::pair<const TypeNode, std::map<Node, Node> >& cm : d_const_map)
220
  {
221
2
    std::vector<Node> consts;
222
2
    for (const std::pair<const Node, Node>& c : cm.second)
223
    {
224
1
      Assert(c.first.isConst());
225
1
      consts.push_back(c.second);
226
    }
227
    // add lemma enforcing introduced constants to be distinct
228
1
    if (consts.size() > 1)
229
    {
230
      Node distinct_const = nm->mkNode(kind::DISTINCT, consts);
231
      Trace("sort-inference-rewrite")
232
          << "Add the constant distinctness lemma: " << std::endl;
233
      Trace("sort-inference-rewrite") << "  " << distinct_const << std::endl;
234
      new_asserts.push_back(distinct_const);
235
    }
236
  }
237
238
  // enforce constraints based on monotonicity
239
12
  Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl;
240
241
14
  for (const std::pair<const TypeNode, std::vector<int> >& tss :
242
12
       d_type_sub_sorts)
243
  {
244
14
    int nmonSort = -1;
245
14
    unsigned nsorts = tss.second.size();
246
26
    for (unsigned i = 0; i < nsorts; i++)
247
    {
248
45
      if (d_non_monotonic_sorts.find(tss.second[i])
249
45
          != d_non_monotonic_sorts.end())
250
      {
251
3
        nmonSort = tss.second[i];
252
3
        break;
253
      }
254
    }
255
14
    if (nmonSort != -1)
256
    {
257
6
      std::vector<Node> injections;
258
6
      TypeNode base_tn = getOrCreateTypeForId(nmonSort, tss.first);
259
7
      for (unsigned i = 0; i < nsorts; i++)
260
      {
261
4
        if (tss.second[i] != nmonSort)
262
        {
263
2
          TypeNode new_tn = getOrCreateTypeForId(tss.second[i], tss.first);
264
          // make injection to nmonSort
265
2
          Node a1 = mkInjection(new_tn, base_tn);
266
1
          injections.push_back(a1);
267
3
          if (d_non_monotonic_sorts.find(tss.second[i])
268
3
              != d_non_monotonic_sorts.end())
269
          {
270
            // also must make injection from nmonSort to this
271
            Node a2 = mkInjection(base_tn, new_tn);
272
            injections.push_back(a2);
273
          }
274
        }
275
      }
276
3
      if (Trace.isOn("sort-inference-rewrite"))
277
      {
278
        Trace("sort-inference-rewrite")
279
            << "Add the following injections for " << tss.first
280
            << " to ensure consistency wrt non-monotonic sorts : " << std::endl;
281
        for (const Node& i : injections)
282
        {
283
          Trace("sort-inference-rewrite") << "   " << i << std::endl;
284
        }
285
      }
286
3
      new_asserts.insert(
287
6
          new_asserts.end(), injections.begin(), injections.end());
288
    }
289
  }
290
12
  Trace("sort-inference-proc") << "...done" << std::endl;
291
  // no sub-sort information is stored
292
12
  reset();
293
12
  Trace("sort-inference-debug") << "Finished sort inference" << std::endl;
294
12
}
295
296
4
void SortInference::computeMonotonicity(const std::vector<Node>& assertions)
297
{
298
8
  std::map<Node, std::map<int, bool> > visitedmt;
299
8
  Trace("sort-inference-proc")
300
4
      << "Calculating monotonicty for types..." << std::endl;
301
18
  for (const Node& a : assertions)
302
  {
303
28
    Trace("sort-inference-debug")
304
14
        << "Process type monotonicity for " << a << std::endl;
305
28
    std::map<Node, Node> var_bound;
306
14
    processMonotonic(a, true, true, var_bound, visitedmt, true);
307
  }
308
4
  Trace("sort-inference-proc") << "...done" << std::endl;
309
4
}
310
311
196
void SortInference::setEqual( int t1, int t2 ){
312
196
  if( t1!=t2 ){
313
124
    int rt1 = d_type_union_find.getRepresentative( t1 );
314
124
    int rt2 = d_type_union_find.getRepresentative( t2 );
315
124
    if( rt1!=rt2 ){
316
76
      Trace("sort-inference-debug") << "Set equal : ";
317
76
      printSort( "sort-inference-debug", rt1 );
318
76
      Trace("sort-inference-debug") << " ";
319
76
      printSort( "sort-inference-debug", rt2 );
320
76
      Trace("sort-inference-debug") << std::endl;
321
      /*
322
      d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() );
323
      d_type_eq_class[rt2].clear();
324
      Trace("sort-inference-debug") << "EqClass : { ";
325
      for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){
326
        Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", ";
327
      }
328
      Trace("sort-inference-debug") << "}" << std::endl;
329
      */
330
76
      if( rt2>rt1 ){
331
        //swap
332
29
        int swap = rt1;
333
29
        rt1 = rt2;
334
29
        rt2 = swap;
335
      }
336
76
      std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 );
337
76
      if( it1!=d_type_types.end() ){
338
7
        if( d_type_types.find( rt2 )==d_type_types.end() ){
339
7
          d_type_types[rt2] = it1->second;
340
7
          d_type_types.erase( rt1 );
341
        }else{
342
          Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl;
343
          return;
344
        }
345
      }
346
76
      d_type_union_find.d_eqc[rt1] = rt2;
347
    }
348
  }
349
}
350
351
158
int SortInference::getIdForType( TypeNode tn ){
352
  //register the return type
353
158
  std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn );
354
158
  if( it==d_id_for_types.end() ){
355
22
    int sc = d_sortCount;
356
22
    d_type_types[d_sortCount] = tn;
357
22
    d_id_for_types[tn] = d_sortCount;
358
22
    d_sortCount++;
359
22
    return sc;
360
  }else{
361
136
    return it->second;
362
  }
363
}
364
365
219
int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< Node, int >& visited ){
366
219
  std::map< Node, int >::iterator itv = visited.find( n );
367
219
  if( itv!=visited.end() ){
368
47
    return itv->second;
369
  }else{
370
    //add to variable bindings
371
172
    bool use_new_visited = false;
372
344
    std::map< Node, int > new_visited;
373
172
    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
374
6
      if( d_var_types.find( n )!=d_var_types.end() ){
375
        return getIdForType( n.getType() );
376
      }else{
377
        //apply sort inference to quantified variables
378
17
        for( size_t i=0; i<n[0].getNumChildren(); i++ ){
379
22
          TypeNode nitn = n[0][i].getType();
380
11
          if( !nitn.isSort() )
381
          {
382
            // If the variable is of an interpreted sort, we assume the
383
            // the sort of the variable will stay the same sort.
384
4
            d_var_types[n][n[0][i]] = getIdForType( nitn );
385
          }
386
          else
387
          {
388
            // If it is of an uninterpreted sort, infer subsorts.
389
7
            d_var_types[n][n[0][i]] = d_sortCount;
390
7
            d_sortCount++;
391
          }
392
11
          var_bound[ n[0][i] ] = n;
393
        }
394
      }
395
6
      use_new_visited = true;
396
    }
397
398
    //process children
399
344
    std::vector< Node > children;
400
344
    std::vector< int > child_types;
401
348
    for( size_t i=0; i<n.getNumChildren(); i++ ){
402
176
      bool processChild = true;
403
176
      if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
404
12
        processChild =
405
12
            options::userPatternsQuant() == options::UserPatMode::IGNORE
406
12
                ? i == 1
407
                : i >= 1;
408
      }
409
176
      if( processChild ){
410
170
        children.push_back( n[i] );
411
170
        child_types.push_back( process( n[i], var_bound, use_new_visited ? new_visited : visited ) );
412
      }
413
    }
414
415
    //remove from variable bindings
416
172
    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
417
      //erase from variable bound
418
17
      for( size_t i=0; i<n[0].getNumChildren(); i++ ){
419
11
        var_bound.erase( n[0][i] );
420
      }
421
    }
422
172
    Trace("sort-inference-debug") << "...Process " << n << std::endl;
423
424
    int retType;
425
172
    if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){
426
28
      Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl;
427
      //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction
428
28
      if( n[0].getType()!=n[1].getType() ){
429
        //for now, assume the original types
430
6
        for( unsigned i=0; i<2; i++ ){
431
4
          int ct = getIdForType( n[i].getType() );
432
4
          setEqual( child_types[i], ct );
433
        }
434
      }else{
435
        //we only require that the left and right hand side must be equal
436
26
        setEqual( child_types[0], child_types[1] );
437
      }
438
28
      d_equality_types[n] = child_types[0];
439
28
      retType = getIdForType( n.getType() );
440
    }
441
144
    else if (isHandledApplyUf(n.getKind()))
442
    {
443
68
      Node op = n.getOperator();
444
68
      TypeNode tn_op = op.getType();
445
34
      if( d_op_return_types.find( op )==d_op_return_types.end() ){
446
7
        if( n.getType().isBoolean() ){
447
          //use booleans
448
          d_op_return_types[op] = getIdForType( n.getType() );
449
        }else{
450
          //assign arbitrary sort for return type
451
7
          d_op_return_types[op] = d_sortCount;
452
7
          d_sortCount++;
453
        }
454
        // d_type_eq_class[d_sortCount].push_back( op );
455
        // assign arbitrary sort for argument types
456
15
        for( size_t i=0; i<n.getNumChildren(); i++ ){
457
8
          d_op_arg_types[op].push_back(d_sortCount);
458
8
          d_sortCount++;
459
        }
460
      }
461
83
      for( size_t i=0; i<n.getNumChildren(); i++ ){
462
        //the argument of the operator must match the return type of the subterm
463
49
        if( n[i].getType()!=tn_op[i] ){
464
          //if type mismatch, assume original types
465
3
          Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType();
466
3
          Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl;
467
3
          int ct1 = getIdForType( n[i].getType() );
468
3
          setEqual( child_types[i], ct1 );
469
3
          int ct2 = getIdForType( tn_op[i] );
470
3
          setEqual( d_op_arg_types[op][i], ct2 );
471
        }else{
472
46
          setEqual( child_types[i], d_op_arg_types[op][i] );
473
        }
474
      }
475
      //return type is the return type
476
34
      retType = d_op_return_types[op];
477
    }else{
478
110
      std::map< Node, Node >::iterator it = var_bound.find( n );
479
110
      if( it!=var_bound.end() ){
480
11
        Trace("sort-inference-debug") << n << " is a bound variable." << std::endl;
481
        //the return type was specified while binding
482
11
        retType = d_var_types[it->second][n];
483
99
      }else if( n.isVar() ){
484
30
        Trace("sort-inference-debug") << n << " is a variable." << std::endl;
485
30
        if( d_op_return_types.find( n )==d_op_return_types.end() ){
486
          //assign arbitrary sort
487
29
          d_op_return_types[n] = d_sortCount;
488
29
          d_sortCount++;
489
          // d_type_eq_class[d_sortCount].push_back( n );
490
        }
491
30
        retType = d_op_return_types[n];
492
69
      }else if( n.isConst() ){
493
30
        Trace("sort-inference-debug") << n << " is a constant." << std::endl;
494
        //can be any type we want
495
30
        retType = d_sortCount;
496
30
        d_sortCount++;
497
      }else{
498
39
        Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl;
499
        //it is an interpreted term
500
104
        for( size_t i=0; i<children.size(); i++ ){
501
65
          Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl;
502
          //must enforce the actual type of the operator on the children
503
65
          int ct = getIdForType( children[i].getType() );
504
65
          setEqual( child_types[i], ct );
505
        }
506
        //return type must be the actual return type
507
39
        retType = getIdForType( n.getType() );
508
      }
509
    }
510
172
    Trace("sort-inference-debug") << "...Type( " << n << " ) = ";
511
172
    printSort("sort-inference-debug", retType );
512
172
    Trace("sort-inference-debug") << std::endl;
513
172
    visited[n] = retType;
514
172
    return retType;
515
  }
516
}
517
518
765
void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, std::map< Node, std::map< int, bool > >& visited, bool typeMode ) {
519
765
  int pindex = hasPol ? ( pol ? 1 : -1 ) : 0;
520
765
  if( visited[n].find( pindex )==visited[n].end() ){
521
575
    visited[n][pindex] = true;
522
575
    Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl;
523
575
    if( n.getKind()==kind::FORALL ){
524
      //only consider variables universally if it is possible this quantified formula is asserted positively
525
32
      if( !hasPol || pol ){
526
37
        for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
527
21
          var_bound[n[0][i]] = n;
528
        }
529
      }
530
32
      processMonotonic( n[1], pol, hasPol, var_bound, visited, typeMode );
531
32
      if( !hasPol || pol ){
532
37
        for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
533
21
          var_bound.erase( n[0][i] );
534
        }
535
      }
536
64
      return;
537
543
    }else if( n.getKind()==kind::EQUAL ){
538
98
      if( !hasPol || pol ){
539
219
        for( unsigned i=0; i<2; i++ ){
540
147
          if( var_bound.find( n[i] )!=var_bound.end() ){
541
3
            if( !typeMode ){
542
3
              int sid = getSortId( var_bound[n[i]], n[i] );
543
3
              d_non_monotonic_sorts[sid] = true;
544
            }else{
545
              d_non_monotonic_sorts_orig[n[i].getType()] = true;
546
            }
547
3
            break;
548
          }
549
        }
550
      }
551
    }
552
1213
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
553
      bool npol;
554
      bool nhasPol;
555
670
      theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol );
556
670
      processMonotonic( n[i], npol, nhasPol, var_bound, visited, typeMode );
557
    }
558
  }
559
}
560
561
562
136
TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){
563
136
  int rt = d_type_union_find.getRepresentative( t );
564
136
  if( d_type_types.find( rt )!=d_type_types.end() ){
565
131
    return d_type_types[rt];
566
  }else{
567
10
    TypeNode retType;
568
    // See if we can assign pref. This is an optimization for reusing an
569
    // uninterpreted sort as the first subsort, so that fewer symbols needed
570
    // to be rewritten in the sort-inferred signature. Notice we only assign
571
    // pref here if it is an uninterpreted sort.
572
15
    if (!pref.isNull() && d_id_for_types.find(pref) == d_id_for_types.end()
573
8
        && pref.isSort())
574
    {
575
1
      retType = pref;
576
    }else{
577
      //must create new type
578
8
      std::stringstream ss;
579
4
      ss << "it_" << t << "_" << pref;
580
4
      retType = NodeManager::currentNM()->mkSort( ss.str() );
581
    }
582
5
    Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
583
5
    printSort("sort-inference", t );
584
5
    Trace("sort-inference") << std::endl;
585
5
    d_id_for_types[ retType ] = rt;
586
5
    d_type_types[ rt ] = retType;
587
5
    return retType;
588
  }
589
}
590
591
49
TypeNode SortInference::getTypeForId( int t ){
592
49
  int rt = d_type_union_find.getRepresentative( t );
593
49
  if( d_type_types.find( rt )!=d_type_types.end() ){
594
49
    return d_type_types[rt];
595
  }else{
596
    return TypeNode::null();
597
  }
598
}
599
600
73
Node SortInference::getNewSymbol( Node old, TypeNode tn ){
601
  // if no sort was inferred for this node, return original
602
73
  if( tn.isNull() || tn.isComparableTo( old.getType() ) ){
603
62
    return old;
604
11
  }else if( old.isConst() ){
605
    //must make constant of type tn
606
1
    if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
607
2
      std::stringstream ss;
608
1
      ss << "ic_" << tn << "_" << old;
609
1
      d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" );  //use mkConst???
610
    }
611
1
    return d_const_map[tn][ old ];
612
10
  }else if( old.getKind()==kind::BOUND_VARIABLE ){
613
6
    std::stringstream ss;
614
3
    ss << "b_" << old;
615
3
    return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
616
  }else{
617
14
    std::stringstream ss;
618
7
    ss << "i_" << old;
619
7
    return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
620
  }
621
}
622
623
219
Node SortInference::simplifyNode(
624
    Node n,
625
    std::map<Node, Node>& var_bound,
626
    TypeNode tnn,
627
    std::map<Node, Node>& model_replace_f,
628
    std::map<Node, std::map<TypeNode, Node> >& visited)
629
{
630
219
  std::map< TypeNode, Node >::iterator itv = visited[n].find( tnn );
631
219
  if( itv!=visited[n].end() ){
632
43
    return itv->second;
633
  }else{
634
176
    Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl;
635
352
    std::vector< Node > children;
636
352
    std::map< Node, std::map< TypeNode, Node > > new_visited;
637
176
    bool use_new_visited = false;
638
176
    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
639
      //recreate based on types of variables
640
12
      std::vector< Node > new_children;
641
17
      for( size_t i=0; i<n[0].getNumChildren(); i++ ){
642
22
        TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() );
643
22
        Node v = getNewSymbol( n[0][i], tn );
644
11
        Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl;
645
11
        new_children.push_back( v );
646
11
        var_bound[ n[0][i] ] = v;
647
      }
648
6
      children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
649
6
      use_new_visited = true;
650
    }
651
652
    //process children
653
176
    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
654
36
      children.push_back( n.getOperator() );
655
    }
656
352
    Node op;
657
176
    if( n.hasOperator() ){
658
101
      op = n.getOperator();
659
    }
660
176
    bool childChanged = false;
661
352
    TypeNode tnnc;
662
352
    for( size_t i=0; i<n.getNumChildren(); i++ ){
663
176
      bool processChild = true;
664
176
      if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
665
12
        processChild =
666
12
            options::userPatternsQuant() == options::UserPatMode::IGNORE
667
24
                ? i == 1
668
12
                : i >= 1;
669
      }
670
176
      if( processChild ){
671
170
        if (isHandledApplyUf(n.getKind()))
672
        {
673
49
          Assert(d_op_arg_types.find(op) != d_op_arg_types.end());
674
49
          tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
675
49
          Assert(!tnnc.isNull());
676
        }
677
318
        else if (n.getKind() == kind::EQUAL && !n[0].getType().isBoolean()
678
298
                 && i == 0)
679
        {
680
28
          Assert(d_equality_types.find(n) != d_equality_types.end());
681
28
          tnnc = getOrCreateTypeForId( d_equality_types[n], n[0].getType() );
682
28
          Assert(!tnnc.isNull());
683
        }
684
        Node nc = simplifyNode(n[i],
685
                               var_bound,
686
                               tnnc,
687
                               model_replace_f,
688
340
                               use_new_visited ? new_visited : visited);
689
170
        Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl;
690
170
        children.push_back( nc );
691
170
        childChanged = childChanged || nc!=n[i];
692
      }
693
    }
694
695
    //remove from variable bindings
696
352
    Node ret;
697
176
    if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
698
      //erase from variable bound
699
17
      for( size_t i=0; i<n[0].getNumChildren(); i++ ){
700
11
        Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
701
11
        var_bound.erase( n[0][i] );
702
      }
703
6
      ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
704
170
    }else if( n.getKind()==kind::EQUAL ){
705
76
      TypeNode tn1 = children[0].getType();
706
76
      TypeNode tn2 = children[1].getType();
707
38
      if( !tn1.isComparableTo( tn2 ) ){
708
        Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl;
709
        Trace("sort-inference-warn") << "  Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
710
        Assert(false);
711
      }
712
38
      ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children );
713
    }
714
132
    else if (isHandledApplyUf(n.getKind()))
715
    {
716
34
      if( d_symbol_map.find( op )==d_symbol_map.end() ){
717
        //make the new operator if necessary
718
7
        bool opChanged = false;
719
14
        std::vector< TypeNode > argTypes;
720
15
        for( size_t i=0; i<n.getNumChildren(); i++ ){
721
16
          TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
722
8
          argTypes.push_back( tn );
723
8
          if( tn!=n[i].getType() ){
724
2
            opChanged = true;
725
          }
726
        }
727
14
        TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() );
728
7
        if( retType!=n.getType() ){
729
3
          opChanged = true;
730
        }
731
7
        if( opChanged ){
732
10
          std::stringstream ss;
733
5
          ss << "io_" << op;
734
10
          TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
735
5
          d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
736
5
          Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl;
737
5
          model_replace_f[op] = d_symbol_map[op];
738
        }else{
739
2
          d_symbol_map[op] = op;
740
        }
741
      }
742
34
      children[0] = d_symbol_map[op];
743
      // make sure all children have been given proper types
744
83
      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
745
      {
746
98
        TypeNode tn = children[i+1].getType();
747
98
        TypeNode tna = getTypeForId( d_op_arg_types[op][i] );
748
49
        if (!tn.isSubtypeOf(tna))
749
        {
750
          Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl;
751
          Assert(false);
752
        }
753
      }
754
34
      ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
755
    }else{
756
98
      std::map< Node, Node >::iterator it = var_bound.find( n );
757
98
      if( it!=var_bound.end() ){
758
12
        ret = it->second;
759
86
      }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){
760
30
        if( d_symbol_map.find( n )==d_symbol_map.end() ){
761
58
          TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() );
762
29
          d_symbol_map[n] = getNewSymbol( n, tn );
763
        }
764
30
        ret = d_symbol_map[n];
765
56
      }else if( n.isConst() ){
766
        //type is determined by context
767
33
        ret = getNewSymbol( n, tnn );
768
23
      }else if( childChanged ){
769
12
        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
770
      }else{
771
11
        ret = n;
772
      }
773
    }
774
176
    visited[n][tnn] = ret;
775
176
    return ret;
776
  }
777
}
778
779
1
Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
780
2
  std::vector< TypeNode > tns;
781
1
  tns.push_back( tn1 );
782
2
  TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
783
2
  Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" );
784
1
  Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
785
2
  Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
786
2
  Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
787
  Node ret = NodeManager::currentNM()->mkNode( kind::FORALL,
788
2
               NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
789
5
               NodeManager::currentNM()->mkNode( kind::OR,
790
2
                 NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(),
791
6
                 v1.eqNode( v2 ) ) );
792
1
  ret = theory::Rewriter::rewrite( ret );
793
2
  return ret;
794
}
795
796
48
int SortInference::getSortId( Node n ) {
797
96
  Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
798
48
  if( d_op_return_types.find( op )!=d_op_return_types.end() ){
799
    return d_type_union_find.getRepresentative( d_op_return_types[op] );
800
  }else{
801
48
    return 0;
802
  }
803
}
804
805
3
int SortInference::getSortId( Node f, Node v ) {
806
3
  if( d_var_types.find( f )!=d_var_types.end() ){
807
3
    return d_type_union_find.getRepresentative( d_var_types[f][v] );
808
  }else{
809
    return 0;
810
  }
811
}
812
813
void SortInference::setSkolemVar( Node f, Node v, Node sk ){
814
  Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl;
815
  if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){
816
    //calculate the sort for variables if not done so already
817
    std::map< Node, Node > var_bound;
818
    std::map< Node, int > visited;
819
    process( f, var_bound, visited );
820
  }
821
  d_op_return_types[sk] = getSortId( f, v );
822
  Trace("sort-inference-temp") << "Set skolem sort id for " << sk << " to " << d_op_return_types[sk] << std::endl;
823
}
824
825
bool SortInference::isWellSortedFormula( Node n ) {
826
  if (n.getType().isBoolean() && !isHandledApplyUf(n.getKind()))
827
  {
828
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
829
      if( !isWellSortedFormula( n[i] ) ){
830
        return false;
831
      }
832
    }
833
    return true;
834
  }else{
835
    return isWellSorted( n );
836
  }
837
}
838
839
bool SortInference::isWellSorted( Node n ) {
840
  if( getSortId( n )==0 ){
841
    return false;
842
  }else{
843
    if (isHandledApplyUf(n.getKind()))
844
    {
845
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
846
        int s1 = getSortId( n[i] );
847
        int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] );
848
        if( s1!=s2 ){
849
          return false;
850
        }
851
        if( !isWellSorted( n[i] ) ){
852
          return false;
853
        }
854
      }
855
    }
856
    return true;
857
  }
858
}
859
860
bool SortInference::isMonotonic( TypeNode tn ) {
861
  Assert(tn.isSort());
862
  return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
863
}
864
865
446
bool SortInference::isHandledApplyUf(Kind k) const
866
{
867
446
  return k == APPLY_UF && !options::ufHo();
868
}
869
870
}  // namespace theory
871
26685
}  // namespace CVC4