GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp Lines: 496 610 81.3 %
Date: 2021-03-22 Branches: 1314 3146 41.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ce_guided_single_inv_sol.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 utility for processing single invocation synthesis conjectures
13
 **
14
 **/
15
#include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/node_algorithm.h"
20
#include "options/quantifiers_options.h"
21
#include "smt/command.h"
22
#include "theory/arith/arith_msum.h"
23
#include "theory/quantifiers/ematching/trigger.h"
24
#include "theory/quantifiers/first_order_model.h"
25
#include "theory/quantifiers/quantifiers_attributes.h"
26
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
27
#include "theory/quantifiers/sygus/synth_engine.h"
28
#include "theory/quantifiers/sygus/term_database_sygus.h"
29
#include "theory/quantifiers/term_enumeration.h"
30
#include "theory/quantifiers/term_util.h"
31
#include "theory/quantifiers_engine.h"
32
#include "theory/rewriter.h"
33
34
using namespace CVC4::kind;
35
using namespace std;
36
37
namespace CVC4 {
38
namespace theory {
39
namespace quantifiers {
40
41
48
bool doCompare(Node a, Node b, Kind k)
42
{
43
96
  Node com = NodeManager::currentNM()->mkNode(k, a, b);
44
48
  com = Rewriter::rewrite(com);
45
48
  Assert(com.getType().isBoolean());
46
96
  return com.isConst() && com.getConst<bool>();
47
}
48
49
2190
CegSingleInvSol::CegSingleInvSol(QuantifiersEngine* qe)
50
2190
    : d_qe(qe), d_id_count(0), d_root_id()
51
{
52
2190
}
53
54
16
void CegSingleInvSol::preregisterConjecture(Node q)
55
{
56
16
  Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
57
32
  Node n = q;
58
16
  if( n.getKind()==FORALL ){
59
16
    n = n[1];
60
  }
61
16
  if( n.getKind()==EXISTS ){
62
    if( n[0].getNumChildren()==d_varList.size() ){
63
      std::vector< Node > evars;
64
      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
65
        evars.push_back( n[0][i] );
66
      }
67
      n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
68
    }else{
69
      Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
70
      return;
71
    }
72
  }
73
16
  Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
74
16
  registerEquivalentTerms( n );
75
}
76
77
16
Node CegSingleInvSol::reconstructSolution(Node sol,
78
                                          TypeNode stn,
79
                                          int& reconstructed,
80
                                          int enumLimit)
81
{
82
16
  Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
83
  int status;
84
16
  d_root_id = collectReconstructNodes( sol, stn, status );
85
16
  if( status==0 ){
86
20
    Node ret = getReconstructedSolution( d_root_id );
87
10
    Trace("csi-rcons") << "Sygus solution is : " << ret << std::endl;
88
10
    Assert(!ret.isNull());
89
10
    reconstructed = 1;
90
10
    return ret;
91
  }
92
6
  if (Trace.isOn("csi-rcons"))
93
  {
94
    for (std::map<TypeNode, std::map<Node, int> >::iterator it =
95
             d_rcons_to_id.begin();
96
         it != d_rcons_to_id.end();
97
         ++it)
98
    {
99
      TypeNode tn = it->first;
100
      Assert(tn.isDatatype());
101
      const DType& dt = tn.getDType();
102
      Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName()
103
                         << " : " << std::endl;
104
      for (std::map<Node, int>::iterator it2 = it->second.begin();
105
           it2 != it->second.end();
106
           ++it2)
107
      {
108
        if (d_reconstruct.find(it2->second) == d_reconstruct.end())
109
        {
110
          Trace("csi-rcons") << "  " << it2->first << std::endl;
111
        }
112
      }
113
      Assert(!it->second.empty());
114
    }
115
  }
116
6
  if (enumLimit != 0)
117
  {
118
6
    int index = 0;
119
6
    std::map< TypeNode, bool > active;
120
13
    for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
121
7
      active[it->first] = true;
122
    }
123
    //enumerate for all types
124
1595
    do {
125
3196
      std::vector< TypeNode > to_erase;
126
3213
      for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){
127
3230
        TypeNode tn = it->first;
128
3230
        Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(tn, index);
129
1618
        if( ns.isNull() ){
130
          to_erase.push_back(tn);
131
        }else{
132
3230
          Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin(ns, tn);
133
3230
          Node nr = Rewriter::rewrite(nb);  // d_qe->getTermDatabaseSygus()->getNormalized(
134
                                            // tn, nb, false, false );
135
3236
          Trace("csi-rcons-debug2")
136
1618
              << "  - try " << ns << " -> " << nr << " for " << tn << " "
137
1618
              << nr.getKind() << std::endl;
138
1618
          std::map<Node, int>::iterator itt = d_rcons_to_id[tn].find(nr);
139
1618
          if (itt != d_rcons_to_id[tn].end())
140
          {
141
            // if it is not already reconstructed
142
10
            if (d_reconstruct.find(itt->second) == d_reconstruct.end())
143
            {
144
12
              Trace("csi-rcons") << "...reconstructed " << ns << " for term "
145
6
                                 << nr << std::endl;
146
6
              setReconstructed(itt->second, ns);
147
12
              Trace("csi-rcons-debug")
148
6
                  << "...path to root, try reconstruction." << std::endl;
149
6
              d_tmp_fail.clear();
150
6
              Node ret = getReconstructedSolution(d_root_id);
151
6
              if (!ret.isNull())
152
              {
153
12
                Trace("csi-rcons")
154
6
                    << "Sygus solution (after enumeration) is : " << ret
155
6
                    << std::endl;
156
6
                reconstructed = 1;
157
6
                return ret;
158
              }
159
            }
160
          }
161
        }
162
      }
163
1595
      for( unsigned i=0; i<to_erase.size(); i++ ){
164
        active.erase( to_erase[i] );
165
      }
166
1595
      index++;
167
1595
      if( index%100==0 ){
168
15
        Trace("csi-rcons-stats") << "Tried " << index << " for each type."  << std::endl;
169
      }
170
1595
    } while (!active.empty() && (enumLimit < 0 || index < enumLimit));
171
  }
172
173
  // we ran out of elements, return null
174
  reconstructed = -1;
175
  Warning() << CommandFailure(
176
      "Cannot get synth function: reconstruction to syntax failed.");
177
  // could return sol here, however, we choose to fail by returning null, since
178
  // it indicates a failure.
179
  return Node::null();
180
}
181
182
411
int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
183
{
184
411
  std::map< Node, int >::iterator itri = d_rcons_to_status[stn].find( t );
185
411
  if( itri!=d_rcons_to_status[stn].end() ){
186
75
    status = itri->second;
187
    //Trace("csi-rcons-debug") << "-> (cached) " << status << " for " << d_rcons_to_id[stn][t] << std::endl;
188
75
    return d_rcons_to_id[stn][t];
189
  }else{
190
336
    status = 1;
191
    // register the type
192
336
    registerType(stn);
193
336
    int id = allocate( t, stn );
194
336
    d_rcons_to_status[stn][t] = -1;
195
672
    TypeNode tn = t.getType();
196
336
    Assert(stn.isDatatype());
197
336
    const DType& dt = stn.getDType();
198
336
    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
199
336
    SygusTypeInfo& sti = tds->getTypeInfo(stn);
200
336
    Assert(dt.isSygus());
201
336
    Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
202
336
    int carg = -1;
203
336
    int karg = -1;
204
    // first, do standard minimizations
205
672
    Node min_t = minimizeBuiltinTerm(t);
206
336
    Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
207
    //check if op is in syntax sort
208
209
336
    carg = sti.getOpConsNum(min_t);
210
336
    if( carg!=-1 ){
211
22
      Trace("csi-rcons-debug") << "  Type has operator." << std::endl;
212
44
      d_reconstruct[id] = NodeManager::currentNM()->mkNode(
213
44
          APPLY_CONSTRUCTOR, dt[carg].getConstructor());
214
22
      status = 0;
215
    }else{
216
      //check if kind is in syntax sort
217
314
      karg = sti.getKindConsNum(min_t.getKind());
218
314
      if( karg!=-1 ){
219
        //collect the children of min_t
220
330
        std::vector< Node > tchildren;
221
165
        if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
222
6
          tchildren.push_back( min_t[0] );
223
12
          std::vector< Node > rem_children;
224
20
          for( unsigned i=1; i<min_t.getNumChildren(); i++ ){
225
14
            rem_children.push_back( min_t[i] );
226
          }
227
12
          Node t2 = NodeManager::currentNM()->mkNode( min_t.getKind(), rem_children );
228
6
          tchildren.push_back( t2 );
229
6
          Trace("csi-rcons-debug") << "...split n-ary to binary " << min_t[0] << " " << t2 << "." << std::endl;
230
        }else{
231
397
          for( unsigned i=0; i<min_t.getNumChildren(); i++ ){
232
238
            tchildren.push_back( min_t[i] );
233
          }
234
        }
235
        //recurse on the children
236
165
        if( tchildren.size()==dt[karg].getNumArgs() ){
237
165
          Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", recurse." << std::endl;
238
165
          status = 0;
239
330
          Node cons = dt[karg].getConstructor();
240
165
          if( !collectReconstructNodes( id, tchildren, dt[karg], d_reconstruct_op[id][cons], status ) ){
241
8
            Trace("csi-rcons-debug") << "...failure for " << id << " " << dt[karg].getName() << std::endl;
242
8
            d_reconstruct_op[id].erase( cons );
243
8
            status = 1;
244
          }
245
        }else{
246
          Trace("csi-rcons-debug") << "Type for " << id << " has kind " << min_t.getKind() << ", but argument # mismatch." << std::endl;
247
        }
248
      }
249
314
      if( status!=0 ){
250
        //try constant reconstruction
251
161
        if( min_t.isConst() ){
252
7
          Trace("csi-rcons-debug") << "...try constant reconstruction." << std::endl;
253
14
          Node min_t_c = builtinToSygusConst(min_t, stn);
254
7
          if( !min_t_c.isNull() ){
255
4
            Trace("csi-rcons-debug") << "   constant reconstruction success for " << id << ", result = " << min_t_c << std::endl;
256
4
            d_reconstruct[id] = min_t_c;
257
4
            status = 0;
258
          }
259
        }
260
161
        if( status!=0 ){
261
          //try identity functions
262
157
          for (unsigned ii : d_id_funcs[stn])
263
          {
264
28
            Assert(dt[ii].getNumArgs() == 1);
265
            //try to directly reconstruct from single argument
266
28
            std::vector< Node > tchildren;
267
28
            tchildren.push_back( min_t );
268
28
            TypeNode stnc = dt[ii][0].getRangeType();
269
28
            Trace("csi-rcons-debug") << "...try identity function " << dt[ii].getSygusOp() << ", child type is " << stnc << std::endl;
270
28
            status = 0;
271
28
            Node cons = dt[ii].getConstructor();
272
28
            if( !collectReconstructNodes( id, tchildren, dt[ii], d_reconstruct_op[id][cons], status ) ){
273
              d_reconstruct_op[id].erase( cons );
274
              status = 1;
275
            }else{
276
28
              Trace("csi-rcons-debug") << "   identity function success for " << id << std::endl;
277
28
              break;
278
            }
279
          }
280
157
          if( status!=0 ){
281
            //try other options, such as matching against other constructors
282
153
            Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
283
            bool success;
284
153
            int c_index = 0;
285
            do{
286
153
              success = false;
287
              int index_found;
288
306
              std::vector< Node > args;
289
153
              if (getMatch(min_t, stn, index_found, args, karg, c_index))
290
              {
291
                success = true;
292
                status = 0;
293
                Node cons = dt[index_found].getConstructor();
294
                Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
295
                for( unsigned i=0; i<args.size(); i++ ){
296
                  Trace("csi-rcons-debug") << "  " << args[i] << std::endl;
297
                }
298
                if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
299
                  d_reconstruct_op[id].erase( cons );
300
                  status = 1;
301
                }else{
302
                  c_index = index_found+1;
303
                }
304
              }
305
153
            }while( success && status!=0 );
306
307
153
            if( status!=0 ){
308
              // construct an equivalence class of terms that are equivalent to t
309
153
              if( d_rep[id]==id ){
310
94
                Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
311
                //get equivalence class of term
312
188
                std::vector< Node > equiv;
313
94
                if( tn.isBoolean() ){
314
176
                  Node curr = min_t;
315
176
                  Node new_t;
316
113
                  do{
317
201
                    new_t = Node::null();
318
201
                    if( curr.getKind()==EQUAL ){
319
19
                      if( curr[0].getType().isInteger() || curr[0].getType().isReal() ){
320
                        new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
321
                                                                      NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
322
19
                      }else if( curr[0].getType().isBoolean() ){
323
38
                        new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
324
38
                                                                      NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
325
                      }else{
326
                        new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
327
                      }
328
182
                    }else if( curr.getKind()==ITE ){
329
                      new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
330
                                                                    NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
331
182
                    }else if( curr.getKind()==OR || curr.getKind()==AND ){
332
83
                      new_t = TermUtil::simpleNegate( curr ).negate();
333
99
                    }else if( curr.getKind()==NOT ){
334
90
                      new_t = TermUtil::simpleNegate( curr[0] );
335
                    }else{
336
9
                      new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
337
                    }
338
201
                    if( !new_t.isNull() ){
339
201
                      if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
340
113
                        curr = new_t;
341
113
                        equiv.push_back( new_t );
342
                      }else{
343
88
                        new_t = Node::null();
344
                      }
345
                    }
346
201
                  }while( !new_t.isNull() );
347
                }
348
                //get decompositions
349
498
                for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
350
404
                  Kind k = sti.getConsNumKind(i);
351
404
                  getEquivalentTerms( k, min_t, equiv );
352
                }
353
                //assign ids to terms
354
94
                Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
355
188
                std::vector< int > equiv_ids;
356
309
                for( unsigned i=0; i<equiv.size(); i++ ){
357
215
                  Trace("csi-rcons-debug") << "  " << equiv[i] << std::endl;
358
215
                  if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
359
207
                    int eq_id = allocate( equiv[i], stn );
360
207
                    d_eqc.erase( eq_id );
361
207
                    d_rep[eq_id] = id;
362
207
                    d_eqc[id].push_back( eq_id );
363
207
                    equiv_ids.push_back( eq_id );
364
                  }else{
365
8
                    equiv_ids.push_back( -1 );
366
                  }
367
                }
368
                // now, try each of them
369
161
                for( unsigned i=0; i<equiv.size(); i++ ){
370
132
                  if( equiv_ids[i]!=-1 ){
371
124
                    collectReconstructNodes( equiv[i], stn, status );
372
                    //if one succeeds
373
124
                    if( status==0 ){
374
130
                      Node rsol = getReconstructedSolution( equiv_ids[i] );
375
65
                      Assert(!rsol.isNull());
376
                      //set all members of the equivalence class that this is the reconstructed solution
377
65
                      setReconstructed( id, rsol );
378
65
                      break;
379
                    }
380
                  }
381
                }
382
              }else{
383
59
                Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
384
              }
385
            }
386
          }
387
        }
388
      }
389
    }
390
336
    if( status!=0 ){
391
88
      Trace("csi-rcons-debug") << "-> *** reconstruction required for id " << id << std::endl;
392
    }else{
393
248
      Trace("csi-rcons-debug") << "-> success for " << id << std::endl;
394
    }
395
336
    d_rcons_to_status[stn][t] = status;
396
336
    return id;
397
  }
398
}
399
400
193
bool CegSingleInvSol::collectReconstructNodes(int pid,
401
                                              std::vector<Node>& ts,
402
                                              const DTypeConstructor& dtc,
403
                                              std::vector<int>& ids,
404
                                              int& status)
405
{
406
193
  Assert(dtc.getNumArgs() == ts.size());
407
456
  for( unsigned i=0; i<ts.size(); i++ ){
408
534
    TypeNode cstn = d_qe->getTermDatabaseSygus()->getArgType( dtc, i );
409
    int cstatus;
410
271
    int c_id = collectReconstructNodes( ts[i], cstn, cstatus );
411
271
    if( cstatus==-1 ){
412
8
      return false;
413
263
    }else if( cstatus!=0 ){
414
28
      status = 1;
415
    }
416
263
    ids.push_back( c_id );
417
  }
418
448
  for( unsigned i=0; i<ids.size(); i++ ){
419
263
    d_parents[ids[i]].push_back( pid );
420
  }
421
185
  return true;
422
}
423
424
316
Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
425
                                                                bool mod_eq)
426
{
427
316
  std::map< int, Node >::iterator it = d_reconstruct.find( id );
428
316
  if( it!=d_reconstruct.end() ){
429
159
    return it->second;
430
  }else{
431
157
    if( std::find( d_tmp_fail.begin(), d_tmp_fail.end(), id )!=d_tmp_fail.end() ){
432
      return Node::null();
433
    }else{
434
      // try each child option
435
157
      std::map< int, std::map< Node, std::vector< int > > >::iterator ito = d_reconstruct_op.find( id );
436
157
      if( ito!=d_reconstruct_op.end() ){
437
157
        for( std::map< Node, std::vector< int > >::iterator itt = ito->second.begin(); itt != ito->second.end(); ++itt ){
438
157
          std::vector< Node > children;
439
157
          children.push_back( itt->first );
440
157
          bool success = true;
441
392
          for( unsigned i=0; i<itt->second.size(); i++ ){
442
470
            Node nc = getReconstructedSolution( itt->second[i] );
443
235
            if( nc.isNull() ){
444
              success = false;
445
              break;
446
            }else{
447
235
              children.push_back( nc );
448
            }
449
          }
450
157
          if( success ){
451
314
            Node ret = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
452
157
            setReconstructed( id, ret );
453
157
            return ret;
454
          }
455
        }
456
      }
457
      // try terms in the equivalence class of this
458
      if( mod_eq ){
459
        int rid = d_rep[id];
460
        for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
461
          int tid = d_eqc[rid][i];
462
          if( tid!=id ){
463
            Node eret = getReconstructedSolution( tid, false );
464
            if( !eret.isNull() ){
465
              setReconstructed( id, eret );
466
              return eret;
467
            }
468
          }
469
        }
470
      }
471
      d_tmp_fail.push_back( id );
472
      return Node::null();
473
    }
474
  }
475
}
476
477
543
int CegSingleInvSol::allocate(Node n, TypeNode stn)
478
{
479
543
  std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n );
480
543
  if( it==d_rcons_to_id[stn].end() ){
481
419
    int ret = d_id_count;
482
419
    if( Trace.isOn("csi-rcons-debug") ){
483
      const DType& dt = stn.getDType();
484
      Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " <<  dt.getName() << std::endl;
485
    }
486
419
    d_id_node[d_id_count] = n;
487
419
    d_id_type[d_id_count] = stn;
488
419
    d_rep[d_id_count] = d_id_count;
489
419
    d_eqc[d_id_count].push_back( d_id_count );
490
419
    d_rcons_to_id[stn][n] = d_id_count;
491
419
    d_id_count++;
492
419
    return ret;
493
  }else{
494
124
    return it->second;
495
  }
496
}
497
498
bool CegSingleInvSol::getPathToRoot(int id)
499
{
500
  if( id==d_root_id ){
501
    return true;
502
  }else{
503
    std::map< int, Node >::iterator it = d_reconstruct.find( id );
504
    if( it!=d_reconstruct.end() ){
505
      return false;
506
    }else{
507
      int rid = d_rep[id];
508
      for( unsigned j=0; j<d_parents[rid].size(); j++ ){
509
        if( getPathToRoot( d_parents[rid][j] ) ){
510
          return true;
511
        }
512
      }
513
      return false;
514
    }
515
  }
516
}
517
518
228
void CegSingleInvSol::setReconstructed(int id, Node n)
519
{
520
  //set all equivalent to this as reconstructed
521
228
  int rid = d_rep[id];
522
806
  for( unsigned i=0; i<d_eqc[rid].size(); i++ ){
523
578
    d_reconstruct[d_eqc[rid][i]] = n;
524
  }
525
228
}
526
527
404
void CegSingleInvSol::getEquivalentTerms(Kind k,
528
                                         Node n,
529
                                         std::vector<Node>& equiv)
530
{
531
404
  if( k==AND || k==OR ){
532
48
    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
533
48
    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
534
  }
535
  //multiplication for integers
536
  //TODO for bitvectors
537
404
  Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND;
538
404
  if( mk!=UNDEFINED_KIND ){
539
5
    if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){
540
1
      bool success = true;
541
3
      for( unsigned i=0; i<2; i++ ){
542
4
        Node eq;
543
2
        if( k==PLUS || k==MINUS ){
544
4
          Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) );
545
2
          eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth );
546
        }
547
2
        if( !eq.isNull() ){
548
2
          eq = Rewriter::rewrite( eq );
549
2
          if (!eq.isConst() || !eq.getConst<bool>())
550
          {
551
            success = false;
552
            break;
553
          }
554
        }
555
      }
556
1
      if( success ){
557
2
        Node var = n[1];
558
2
        Node rem;
559
1
        if( k==PLUS || k==MINUS ){
560
1
          int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt();
561
1
          if( rem_coeff>0 && k==PLUS ){
562
            rem_coeff--;
563
1
          }else if( rem_coeff<0 && k==MINUS ){
564
            rem_coeff++;
565
          }else{
566
1
            success = false;
567
          }
568
1
          if( success ){
569
            rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var );
570
            rem = Rewriter::rewrite( rem );
571
          }
572
        }
573
1
        if( !rem.isNull() ){
574
          equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) );
575
        }
576
      }
577
    }
578
  }
579
  //negative constants
580
404
  if( k==MINUS ){
581
4
    if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){
582
2
      Node nn = NodeManager::currentNM()->mkNode( UMINUS, n );
583
1
      nn = Rewriter::rewrite( nn );
584
1
      equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
585
    }
586
  }
587
  //inequalities
588
404
  if( k==GEQ || k==LEQ || k==LT || k==GT || k==NOT ){
589
150
    Node atom = n.getKind()==NOT ? n[0] : n;
590
75
    bool pol = n.getKind()!=NOT;
591
75
    Kind ak = atom.getKind();
592
75
    if( ( ak==GEQ || ak==LEQ || ak==LT || ak==GT ) && ( pol || k!=NOT ) ){
593
10
      Node t1 = atom[0];
594
10
      Node t2 = atom[1];
595
5
      if( !pol ){
596
1
        ak = ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) );
597
      }
598
5
      if( k==NOT ){
599
2
        equiv.push_back( NodeManager::currentNM()->mkNode( ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ), t1, t2 ).negate() );
600
3
      }else if( k==ak ){
601
        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
602
3
      }else if( (k==GEQ || k==LEQ)==(ak==GEQ || ak==LEQ) ){
603
2
        equiv.push_back( NodeManager::currentNM()->mkNode( k, t2, t1 ) );
604
1
      }else if( t1.getType().isInteger() && t2.getType().isInteger() ){
605
1
        if( (k==GEQ || k==GT)!=(ak==GEQ || ak==GT) ){
606
          Node ts = t1;
607
          t1 = t2;
608
          t2 = ts;
609
          ak = ak==GEQ ? LEQ : ( ak==LEQ ? GEQ : ( ak==LT ? GT : LT ) );
610
        }
611
1
        t2 = NodeManager::currentNM()->mkNode( PLUS, t2, NodeManager::currentNM()->mkConst( Rational( (ak==GT || ak==LEQ) ? 1 : -1 ) ) );
612
1
        t2 = Rewriter::rewrite( t2 );
613
1
        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
614
      }
615
    }
616
  }
617
618
  //based on eqt cache
619
404
  std::map< Node, Node >::iterator itet = d_eqt_rep.find( n );
620
404
  if( itet!=d_eqt_rep.end() ){
621
    Node rn = itet->second;
622
    for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){
623
      if( d_eqt_eqc[rn][i]!=n && d_eqt_eqc[rn][i].getKind()==k ){
624
        if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
625
          equiv.push_back( d_eqt_eqc[rn][i] );
626
        }
627
      }
628
    }
629
  }
630
404
}
631
632
376
void CegSingleInvSol::registerEquivalentTerms(Node n)
633
{
634
736
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
635
360
    registerEquivalentTerms( n[i] );
636
  }
637
752
  Node rn = Rewriter::rewrite( n );
638
376
  if( rn!=n ){
639
    Trace("csi-equiv") << "  eq terms : " << n << " " << rn << std::endl;
640
    d_eqt_rep[n] = rn;
641
    d_eqt_rep[rn] = rn;
642
    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
643
      d_eqt_eqc[rn].push_back( rn );
644
    }
645
    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
646
      d_eqt_eqc[rn].push_back( n );
647
    }
648
  }
649
376
}
650
651
46
Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
652
{
653
46
  std::map<Node, Node>::iterator it = d_builtin_const_to_sygus[tn].find(c);
654
46
  if (it != d_builtin_const_to_sygus[tn].end())
655
  {
656
19
    return it->second;
657
  }
658
27
  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
659
27
  NodeManager* nm = NodeManager::currentNM();
660
27
  SygusTypeInfo& ti = tds->getTypeInfo(tn);
661
54
  Node sc;
662
27
  d_builtin_const_to_sygus[tn][c] = sc;
663
27
  Assert(c.isConst());
664
27
  if (!tn.isDatatype())
665
  {
666
    // if we've traversed to a builtin type, simply return c
667
    d_builtin_const_to_sygus[tn][c] = c;
668
    return c;
669
  }
670
27
  const DType& dt = tn.getDType();
671
54
  Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in "
672
27
                           << dt.getName() << std::endl;
673
27
  if (!dt.isSygus())
674
  {
675
    // if we've traversed to a builtin datatype type, simply return c
676
    d_builtin_const_to_sygus[tn][c] = c;
677
    return c;
678
  }
679
  // if we are not interested in reconstructing constants, or the grammar allows
680
  // them, return a proxy
681
54
  if (!options::cegqiSingleInvReconstructConst() || dt.getSygusAllowConst())
682
  {
683
2
    sc = tds->getProxyVariable(tn, c);
684
  }
685
  else
686
  {
687
25
    int carg = ti.getOpConsNum(c);
688
25
    if (carg != -1)
689
    {
690
2
      sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[carg].getConstructor());
691
    }
692
    else
693
    {
694
      // identity functions
695
23
      for (unsigned ii : d_id_funcs[tn])
696
      {
697
1
        Assert(dt[ii].getNumArgs() == 1);
698
        // try to directly reconstruct from single argument
699
1
        TypeNode tnc = tds->getArgType(dt[ii], 0);
700
2
        Trace("csi-rcons-debug")
701
2
            << "Based on id function " << dt[ii].getSygusOp()
702
1
            << ", try reconstructing " << c << " instead in " << tnc
703
1
            << std::endl;
704
1
        Node n = builtinToSygusConst(c, tnc, rcons_depth);
705
1
        if (!n.isNull())
706
        {
707
1
          sc = nm->mkNode(APPLY_CONSTRUCTOR, dt[ii].getConstructor(), n);
708
1
          break;
709
        }
710
      }
711
23
      if (sc.isNull())
712
      {
713
22
        if (rcons_depth < 1000)
714
        {
715
          // accelerated, recursive reconstruction of constants
716
22
          Kind pk = getPlusKind(dt.getSygusType());
717
22
          if (pk != UNDEFINED_KIND)
718
          {
719
20
            int arg = ti.getKindConsNum(pk);
720
20
            if (arg != -1)
721
            {
722
20
              Kind ck = getComparisonKind(dt.getSygusType());
723
20
              Kind pkm = getPlusKind(dt.getSygusType(), true);
724
              // get types
725
20
              Assert(dt[arg].getNumArgs() == 2);
726
40
              TypeNode tn1 = tds->getArgType(dt[arg], 0);
727
40
              TypeNode tn2 = tds->getArgType(dt[arg], 1);
728
              // initialize d_const_list for tn1
729
20
              registerType(tn1);
730
              // iterate over all positive constants, largest to smallest
731
20
              int start = d_const_list[tn1].size() - 1;
732
20
              int end = d_const_list[tn1].size() - d_const_list_pos[tn1];
733
21
              for (int i = start; i >= end; --i)
734
              {
735
21
                Node c1 = d_const_list[tn1][i];
736
                // only consider if smaller than c, and
737
20
                if (doCompare(c1, c, ck))
738
                {
739
19
                  Node c2 = nm->mkNode(pkm, c, c1);
740
19
                  c2 = Rewriter::rewrite(c2);
741
19
                  if (c2.isConst())
742
                  {
743
                    // reconstruct constant on the other side
744
19
                    Node sc2 = builtinToSygusConst(c2, tn2, rcons_depth + 1);
745
19
                    if (!sc2.isNull())
746
                    {
747
38
                      Node sc1 = builtinToSygusConst(c1, tn1, rcons_depth);
748
19
                      Assert(!sc1.isNull());
749
57
                      sc = nm->mkNode(APPLY_CONSTRUCTOR,
750
38
                                      dt[arg].getConstructor(),
751
                                      sc1,
752
                                      sc2);
753
19
                      break;
754
                    }
755
                  }
756
                }
757
              }
758
            }
759
          }
760
        }
761
      }
762
    }
763
  }
764
27
  d_builtin_const_to_sygus[tn][c] = sc;
765
27
  return sc;
766
}
767
768
struct sortConstants
769
{
770
  Kind d_comp_kind;
771
16
  bool operator()(Node i, Node j)
772
  {
773
16
    return i != j && doCompare(i, j, d_comp_kind);
774
  }
775
};
776
777
356
void CegSingleInvSol::registerType(TypeNode tn)
778
{
779
356
  if (d_const_list_pos.find(tn) != d_const_list_pos.end())
780
  {
781
337
    return;
782
  }
783
19
  d_const_list_pos[tn] = 0;
784
19
  Assert(tn.isDatatype());
785
786
19
  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
787
  // ensure it is registered
788
19
  tds->registerSygusType(tn);
789
19
  const DType& dt = tn.getDType();
790
19
  Assert(dt.isSygus());
791
38
  TypeNode btn = dt.getSygusType();
792
  // for constant reconstruction
793
19
  Kind ck = getComparisonKind(btn);
794
38
  Node z = TermUtil::mkTypeValue(btn, 0);
795
796
  // iterate over constructors
797
114
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
798
  {
799
190
    Node n = dt[i].getSygusOp();
800
95
    if (n.getKind() != kind::BUILTIN && n.isConst())
801
    {
802
16
      d_const_list[tn].push_back(n);
803
16
      if (ck != UNDEFINED_KIND && doCompare(z, n, ck))
804
      {
805
6
        d_const_list_pos[tn]++;
806
      }
807
    }
808
95
    if (dt[i].isSygusIdFunc())
809
    {
810
12
      d_id_funcs[tn].push_back(i);
811
    }
812
  }
813
  // sort the constant list
814
19
  if (!d_const_list[tn].empty())
815
  {
816
8
    if (ck != UNDEFINED_KIND)
817
    {
818
      sortConstants sc;
819
8
      sc.d_comp_kind = ck;
820
8
      std::sort(d_const_list[tn].begin(), d_const_list[tn].end(), sc);
821
    }
822
16
    Trace("csi-rcons") << "Type has " << d_const_list[tn].size()
823
8
                       << " constants..." << std::endl
824
8
                       << "  ";
825
24
    for (unsigned i = 0; i < d_const_list[tn].size(); i++)
826
    {
827
16
      Trace("csi-rcons") << d_const_list[tn][i] << " ";
828
    }
829
8
    Trace("csi-rcons") << std::endl;
830
16
    Trace("csi-rcons") << "Of these, " << d_const_list_pos[tn]
831
8
                       << " are marked as positive." << std::endl;
832
  }
833
}
834
835
50
bool CegSingleInvSol::getMatch(Node p,
836
                               Node n,
837
                               std::map<int, Node>& s,
838
                               std::vector<int>& new_s)
839
{
840
50
  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
841
50
  if (tds->isFreeVar(p))
842
  {
843
4
    size_t vnum = tds->getFreeVarId(p);
844
8
    Node prev = s[vnum];
845
4
    s[vnum] = n;
846
4
    if (prev.isNull())
847
    {
848
4
      new_s.push_back(vnum);
849
    }
850
4
    return prev.isNull() || prev == n;
851
  }
852
46
  if (n.getNumChildren() == 0)
853
  {
854
17
    return p == n;
855
  }
856
29
  if (n.getKind() == p.getKind() && n.getNumChildren() == p.getNumChildren())
857
  {
858
    // try both ways?
859
    unsigned rmax =
860
19
        TermUtil::isComm(n.getKind()) && n.getNumChildren() == 2 ? 2 : 1;
861
38
    std::vector<int> new_tmp;
862
43
    for (unsigned r = 0; r < rmax; r++)
863
    {
864
24
      bool success = true;
865
28
      for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
866
      {
867
28
        int io = r == 0 ? i : (i == 0 ? 1 : 0);
868
28
        if (!getMatch(p[i], n[io], s, new_tmp))
869
        {
870
24
          success = false;
871
28
          for (unsigned j = 0; j < new_tmp.size(); j++)
872
          {
873
4
            s.erase(new_tmp[j]);
874
          }
875
24
          new_tmp.clear();
876
24
          break;
877
        }
878
      }
879
24
      if (success)
880
      {
881
        new_s.insert(new_s.end(), new_tmp.begin(), new_tmp.end());
882
        return true;
883
      }
884
    }
885
  }
886
29
  return false;
887
}
888
889
153
bool CegSingleInvSol::getMatch(Node t,
890
                               TypeNode st,
891
                               int& index_found,
892
                               std::vector<Node>& args,
893
                               int index_exc,
894
                               int index_start)
895
{
896
153
  Assert(st.isDatatype());
897
153
  const DType& dt = st.getDType();
898
153
  Assert(dt.isSygus());
899
306
  std::map<Kind, std::vector<Node> > kgens;
900
306
  std::vector<Node> gens;
901
783
  for (unsigned i = index_start, ncons = dt.getNumConstructors(); i < ncons;
902
       i++)
903
  {
904
630
    if ((int)i != index_exc)
905
    {
906
1236
      Node g = getGenericBase(st, dt, i);
907
618
      gens.push_back(g);
908
618
      kgens[g.getKind()].push_back(g);
909
1236
      Trace("csi-sol-debug") << "Check generic base : " << g << " from "
910
618
                             << dt[i].getName() << std::endl;
911
618
      if (g.getKind() == t.getKind())
912
      {
913
44
        Trace("csi-sol-debug") << "Possible match ? " << g << " " << t
914
22
                               << " for " << dt[i].getName() << std::endl;
915
44
        std::map<int, Node> sigma;
916
44
        std::vector<int> new_s;
917
22
        if (getMatch(g, t, sigma, new_s))
918
        {
919
          // we found an exact match
920
          bool msuccess = true;
921
          for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
922
          {
923
            if (sigma[j].isNull())
924
            {
925
              msuccess = false;
926
              break;
927
            }
928
            else
929
            {
930
              args.push_back(sigma[j]);
931
            }
932
          }
933
          if (msuccess)
934
          {
935
            index_found = i;
936
            return true;
937
          }
938
        }
939
      }
940
    }
941
  }
942
153
  return false;
943
}
944
945
618
Node CegSingleInvSol::getGenericBase(TypeNode tn, const DType& dt, int c)
946
{
947
618
  std::map<int, Node>::iterator it = d_generic_base[tn].find(c);
948
618
  if (it != d_generic_base[tn].end())
949
  {
950
564
    return it->second;
951
  }
952
54
  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
953
54
  Assert(tds->isRegistered(tn));
954
108
  Node g = tds->mkGeneric(dt, c);
955
54
  Trace("csi-sol-debug") << "Generic is " << g << std::endl;
956
108
  Node gr = Rewriter::rewrite(g);
957
54
  Trace("csi-sol-debug") << "Generic rewritten is " << gr << std::endl;
958
54
  d_generic_base[tn][c] = gr;
959
54
  return gr;
960
}
961
962
336
Node CegSingleInvSol::minimizeBuiltinTerm(Node n)
963
{
964
336
  Kind nk = n.getKind();
965
653
  if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT)
966
358
      || !n[0].getType().isReal())
967
  {
968
333
    return n;
969
  }
970
3
  NodeManager* nm = NodeManager::currentNM();
971
3
  bool changed = false;
972
6
  std::vector<Node> mon[2];
973
9
  for (unsigned r = 0; r < 2; r++)
974
  {
975
6
    unsigned ro = r == 0 ? 1 : 0;
976
12
    Node c;
977
12
    Node nc;
978
6
    if (n[r].getKind() == PLUS)
979
    {
980
6
      for (unsigned i = 0; i < n[r].getNumChildren(); i++)
981
      {
982
12
        if (ArithMSum::getMonomial(n[r][i], c, nc)
983
12
            && c.getConst<Rational>().isNegativeOne())
984
        {
985
1
          mon[ro].push_back(nc);
986
1
          changed = true;
987
        }
988
        else
989
        {
990
3
          if (!n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero())
991
          {
992
3
            mon[r].push_back(n[r][i]);
993
          }
994
        }
995
      }
996
    }
997
    else
998
    {
999
12
      if (ArithMSum::getMonomial(n[r], c, nc)
1000
12
          && c.getConst<Rational>().isNegativeOne())
1001
      {
1002
        mon[ro].push_back(nc);
1003
        changed = true;
1004
      }
1005
      else
1006
      {
1007
4
        if (!n[r].isConst() || !n[r].getConst<Rational>().isZero())
1008
        {
1009
3
          mon[r].push_back(n[r]);
1010
        }
1011
      }
1012
    }
1013
  }
1014
3
  if (changed)
1015
  {
1016
2
    Node nn[2];
1017
3
    for (unsigned r = 0; r < 2; r++)
1018
    {
1019
4
      nn[r] = mon[r].size() == 0
1020
8
                  ? nm->mkConst(Rational(0))
1021
6
                  : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r]));
1022
    }
1023
1
    return nm->mkNode(n.getKind(), nn[0], nn[1]);
1024
  }
1025
2
  return n;
1026
}
1027
1028
39
Kind CegSingleInvSol::getComparisonKind(TypeNode tn)
1029
{
1030
39
  if (tn.isInteger() || tn.isReal())
1031
  {
1032
31
    return LT;
1033
  }
1034
8
  else if (tn.isBitVector())
1035
  {
1036
1
    return BITVECTOR_ULT;
1037
  }
1038
7
  return UNDEFINED_KIND;
1039
}
1040
1041
42
Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg)
1042
{
1043
42
  if (tn.isInteger() || tn.isReal())
1044
  {
1045
40
    return is_neg ? MINUS : PLUS;
1046
  }
1047
2
  else if (tn.isBitVector())
1048
  {
1049
    return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
1050
  }
1051
2
  return UNDEFINED_KIND;
1052
}
1053
}
1054
}
1055
26676
}