GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_repair_const.cpp Lines: 299 331 90.3 %
Date: 2021-03-22 Branches: 591 1436 41.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_repair_const.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
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 sygus_repair_const
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_repair_const.h"
16
17
#include "api/cvc4cpp.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/node_algorithm.h"
20
#include "options/base_options.h"
21
#include "options/quantifiers_options.h"
22
#include "printer/printer.h"
23
#include "smt/smt_engine.h"
24
#include "smt/smt_engine_scope.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/datatypes/theory_datatypes_utils.h"
27
#include "theory/logic_info.h"
28
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
29
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
30
#include "theory/quantifiers/sygus/term_database_sygus.h"
31
#include "theory/quantifiers_engine.h"
32
#include "theory/smt_engine_subsolver.h"
33
34
using namespace CVC4::kind;
35
36
namespace CVC4 {
37
namespace theory {
38
namespace quantifiers {
39
40
2190
SygusRepairConst::SygusRepairConst(QuantifiersEngine* qe)
41
2190
    : d_qe(qe), d_allow_constant_grammar(false)
42
{
43
2190
  d_tds = d_qe->getTermDatabaseSygus();
44
2190
}
45
46
13
void SygusRepairConst::initialize(Node base_inst,
47
                                  const std::vector<Node>& candidates)
48
{
49
13
  Trace("sygus-repair-const") << "SygusRepairConst::initialize" << std::endl;
50
13
  Trace("sygus-repair-const") << "  conjecture : " << base_inst << std::endl;
51
13
  d_base_inst = base_inst;
52
53
  // compute whether there are "allow all constant" types in the variables of q
54
26
  std::map<TypeNode, bool> tprocessed;
55
26
  for (const Node& v : candidates)
56
  {
57
26
    TypeNode tn = v.getType();
58
    // do the type traversal of the sygus type
59
13
    registerSygusType(tn, tprocessed);
60
  }
61
26
  Trace("sygus-repair-const")
62
13
      << "  allow constants : " << d_allow_constant_grammar << std::endl;
63
13
}
64
65
// recursion depth bounded by number of types in grammar (small)
66
165
void SygusRepairConst::registerSygusType(TypeNode tn,
67
                                         std::map<TypeNode, bool>& tprocessed)
68
{
69
165
  if (tprocessed.find(tn) == tprocessed.end())
70
  {
71
48
    tprocessed[tn] = true;
72
48
    if (!tn.isDatatype())
73
    {
74
      // may have recursed to a non-datatype, e.g. in the case that we have
75
      // "any constant" constructors
76
16
      return;
77
    }
78
32
    const DType& dt = tn.getDType();
79
32
    if (!dt.isSygus())
80
    {
81
      // may have recursed to a non-sygus-datatype
82
      return;
83
    }
84
    // check if this datatype allows all constants
85
32
    if (dt.getSygusAllowConst())
86
    {
87
25
      d_allow_constant_grammar = true;
88
    }
89
169
    for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
90
    {
91
137
      const DTypeConstructor& dtc = dt[i];
92
      // recurse on all subfields
93
289
      for (unsigned j = 0, nargs = dtc.getNumArgs(); j < nargs; j++)
94
      {
95
304
        TypeNode tnc = d_tds->getArgType(dtc, j);
96
152
        registerSygusType(tnc, tprocessed);
97
      }
98
    }
99
  }
100
}
101
102
281
bool SygusRepairConst::isActive() const
103
{
104
281
  return !d_base_inst.isNull() && d_allow_constant_grammar;
105
}
106
107
145
bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
108
                                      const std::vector<Node>& candidate_values,
109
                                      std::vector<Node>& repair_cv,
110
                                      bool useConstantsAsHoles)
111
{
112
290
  return repairSolution(d_base_inst,
113
                        candidates,
114
                        candidate_values,
115
                        repair_cv,
116
290
                        useConstantsAsHoles);
117
}
118
119
281
bool SygusRepairConst::repairSolution(Node sygusBody,
120
                                      const std::vector<Node>& candidates,
121
                                      const std::vector<Node>& candidate_values,
122
                                      std::vector<Node>& repair_cv,
123
                                      bool useConstantsAsHoles)
124
{
125
281
  Assert(candidates.size() == candidate_values.size());
126
127
  // if no grammar type allows constants, no repair is possible
128
281
  if (!isActive())
129
  {
130
    return false;
131
  }
132
281
  if (Trace.isOn("sygus-repair-const"))
133
  {
134
    Trace("sygus-repair-const") << "Repair candidate solutions..." << std::endl;
135
    for (unsigned i = 0, size = candidates.size(); i < size; i++)
136
    {
137
      std::stringstream ss;
138
      TermDbSygus::toStreamSygus(ss, candidate_values[i]);
139
      Trace("sygus-repair-const")
140
          << "  " << candidates[i] << " -> " << ss.str() << std::endl;
141
    }
142
    Trace("sygus-repair-const")
143
        << "Getting candidate skeletons : " << std::endl;
144
  }
145
562
  std::vector<Node> candidate_skeletons;
146
562
  std::map<TypeNode, int> free_var_count;
147
562
  std::vector<Node> sk_vars;
148
562
  std::map<Node, Node> sk_vars_to_subs;
149
562
  for (unsigned i = 0, size = candidates.size(); i < size; i++)
150
  {
151
562
    Node cv = candidate_values[i];
152
    Node skeleton = getSkeleton(
153
562
        cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
154
281
    if (Trace.isOn("sygus-repair-const"))
155
    {
156
      std::stringstream ss;
157
      TermDbSygus::toStreamSygus(ss, cv);
158
      Trace("sygus-repair-const")
159
          << "Solution #" << i << " : " << ss.str() << std::endl;
160
      if (skeleton == cv)
161
      {
162
        Trace("sygus-repair-const") << "...solution unchanged" << std::endl;
163
      }
164
      else
165
      {
166
        std::stringstream sss;
167
        TermDbSygus::toStreamSygus(sss, skeleton);
168
        Trace("sygus-repair-const")
169
            << "...inferred skeleton : " << sss.str() << std::endl;
170
      }
171
    }
172
281
    candidate_skeletons.push_back(skeleton);
173
  }
174
175
281
  if (sk_vars.empty())
176
  {
177
    Trace("sygus-repair-const") << "...no solutions repaired." << std::endl;
178
    return false;
179
  }
180
181
281
  Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
182
  Node fo_body =
183
562
      getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars);
184
185
281
  Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl;
186
187
281
  if (d_queries.find(fo_body) != d_queries.end())
188
  {
189
38
    Trace("sygus-repair-const") << "...duplicate query." << std::endl;
190
38
    return false;
191
  }
192
243
  d_queries.insert(fo_body);
193
194
  // check whether it is not in the current logic, e.g. non-linear arithmetic.
195
  // if so, undo replacements until it is in the current logic.
196
486
  LogicInfo logic = smt::currentSmtEngine()->getLogicInfo();
197
243
  if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear())
198
  {
199
170
    fo_body = fitToLogic(sygusBody,
200
                         logic,
201
                         fo_body,
202
                         candidates,
203
                         candidate_skeletons,
204
                         sk_vars,
205
                         sk_vars_to_subs);
206
340
    Trace("sygus-repair-const-debug")
207
170
        << "...after fit-to-logic : " << fo_body << std::endl;
208
  }
209
243
  Assert(!expr::hasFreeVar(fo_body));
210
211
243
  if (fo_body.isNull() || sk_vars.empty())
212
  {
213
12
    Trace("sygus-repair-const")
214
6
        << "...all skeleton variables lead to bad logic." << std::endl;
215
6
    return false;
216
  }
217
218
237
  Trace("sygus-repair-const") << "Make satisfiabily query..." << std::endl;
219
237
  if (fo_body.getKind() == FORALL)
220
  {
221
    // must be a CBQI quantifier
222
107
    CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body, d_qe);
223
107
    if (hstatus < CEG_HANDLED)
224
    {
225
      // abort if less than fully handled
226
      Trace("sygus-repair-const") << "...first-order query is not handlable by "
227
                                     "counterexample-guided instantiation."
228
                                  << std::endl;
229
      return false;
230
    }
231
  }
232
233
237
  Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
234
  // make the satisfiability query
235
474
  std::unique_ptr<SmtEngine> repcChecker;
236
  // initialize the subsolver using the standard method
237
474
  initializeSubsolver(repcChecker,
238
711
                      options::sygusRepairConstTimeout.wasSetByUser(),
239
237
                      options::sygusRepairConstTimeout());
240
  // renable options disabled by sygus
241
237
  repcChecker->setOption("miniscope-quant", "true");
242
237
  repcChecker->setOption("miniscope-quant-fv", "true");
243
237
  repcChecker->setOption("quant-split", "true");
244
237
  repcChecker->assertFormula(fo_body);
245
  // check satisfiability
246
474
  Result r = repcChecker->checkSat();
247
237
  Trace("sygus-repair-const") << "...got : " << r << std::endl;
248
711
  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
249
711
      || r.asSatisfiabilityResult().isUnknown())
250
  {
251
216
    Trace("sygus-engine") << "...failed" << std::endl;
252
216
    return false;
253
  }
254
42
  std::vector<Node> sk_sygus_m;
255
53
  for (const Node& v : sk_vars)
256
  {
257
32
    Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
258
64
    Node fov = d_sk_to_fo[v];
259
64
    Node fov_m = repcChecker->getValue(fov);
260
32
    Trace("sygus-repair-const") << "  " << fov << " = " << fov_m << std::endl;
261
    // convert to sygus
262
64
    Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m);
263
32
    sk_sygus_m.push_back(fov_m_to_sygus);
264
  }
265
42
  std::stringstream ss;
266
  // convert back to sygus
267
42
  for (unsigned i = 0, size = candidates.size(); i < size; i++)
268
  {
269
42
    Node csk = candidate_skeletons[i];
270
    Node scsk = csk.substitute(
271
42
        sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
272
21
    repair_cv.push_back(scsk);
273
21
    if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
274
    {
275
      std::stringstream sss;
276
      TermDbSygus::toStreamSygus(sss, repair_cv[i]);
277
      ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
278
    }
279
  }
280
21
  Trace("sygus-engine") << "...success:" << std::endl;
281
21
  Trace("sygus-engine") << ss.str();
282
42
  Trace("sygus-repair-const")
283
21
      << "Repaired constants in solution : " << std::endl;
284
21
  Trace("sygus-repair-const") << ss.str();
285
21
  return true;
286
}
287
288
239
bool SygusRepairConst::mustRepair(Node n)
289
{
290
478
  std::unordered_set<TNode, TNodeHashFunction> visited;
291
478
  std::vector<TNode> visit;
292
478
  TNode cur;
293
239
  visit.push_back(n);
294
503
  do
295
  {
296
742
    cur = visit.back();
297
742
    visit.pop_back();
298
742
    if (visited.find(cur) == visited.end())
299
    {
300
674
      visited.insert(cur);
301
674
      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
302
674
      if (isRepairable(cur, false))
303
      {
304
145
        return true;
305
      }
306
1228
      for (const Node& cn : cur)
307
      {
308
699
        visit.push_back(cn);
309
      }
310
    }
311
597
  } while (!visit.empty());
312
313
94
  return false;
314
}
315
316
2297
bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
317
{
318
2297
  if (n.getKind() != APPLY_CONSTRUCTOR)
319
  {
320
321
    return false;
321
  }
322
3952
  TypeNode tn = n.getType();
323
1976
  Assert(tn.isDatatype());
324
1976
  const DType& dt = tn.getDType();
325
1976
  if (!dt.isSygus())
326
  {
327
    return false;
328
  }
329
3952
  Node op = n.getOperator();
330
1976
  unsigned cindex = datatypes::utils::indexOf(op);
331
3952
  Node sygusOp = dt[cindex].getSygusOp();
332
1976
  if (sygusOp.getAttribute(SygusAnyConstAttribute()))
333
  {
334
    // if it represents "any constant" then it is repairable
335
539
    return true;
336
  }
337
1437
  if (dt[cindex].getNumArgs() > 0)
338
  {
339
700
    return false;
340
  }
341
737
  if (useConstantsAsHoles && dt.getSygusAllowConst())
342
  {
343
    if (sygusOp.isConst())
344
    {
345
      // if a constant, it is repairable
346
      return true;
347
    }
348
  }
349
737
  return false;
350
}
351
352
281
Node SygusRepairConst::getSkeleton(Node n,
353
                                   std::map<TypeNode, int>& free_var_count,
354
                                   std::vector<Node>& sk_vars,
355
                                   std::map<Node, Node>& sk_vars_to_subs,
356
                                   bool useConstantsAsHoles)
357
{
358
281
  if (isRepairable(n, useConstantsAsHoles))
359
  {
360
8
    Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
361
4
    sk_vars.push_back(sk_var);
362
4
    sk_vars_to_subs[sk_var] = n;
363
8
    Trace("sygus-repair-const-debug")
364
4
        << "Var to subs : " << sk_var << " -> " << n << std::endl;
365
4
    return sk_var;
366
  }
367
277
  NodeManager* nm = NodeManager::currentNM();
368
  // get the most general candidate skeleton of n
369
554
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
370
277
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
371
554
  std::vector<TNode> visit;
372
554
  TNode cur;
373
277
  visit.push_back(n);
374
2795
  do
375
  {
376
3072
    cur = visit.back();
377
3072
    visit.pop_back();
378
3072
    it = visited.find(cur);
379
380
3072
    if (it == visited.end())
381
    {
382
1453
      visited[cur] = Node::null();
383
1453
      visit.push_back(cur);
384
2795
      for (const Node& cn : cur)
385
      {
386
1342
        visit.push_back(cn);
387
      }
388
    }
389
1619
    else if (it->second.isNull())
390
    {
391
2906
      Node ret = cur;
392
1453
      bool childChanged = false;
393
2906
      std::vector<Node> children;
394
1453
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
395
      {
396
1132
        children.push_back(cur.getOperator());
397
      }
398
2795
      for (const Node& cn : cur)
399
      {
400
2684
        Node child;
401
        // if it is repairable
402
1342
        if (isRepairable(cn, useConstantsAsHoles))
403
        {
404
          // replace it by the next free variable
405
390
          child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
406
390
          sk_vars.push_back(child);
407
390
          sk_vars_to_subs[child] = cn;
408
780
          Trace("sygus-repair-const-debug")
409
390
              << "Var to subs : " << child << " -> " << cn << std::endl;
410
        }
411
        else
412
        {
413
952
          it = visited.find(cn);
414
952
          Assert(it != visited.end());
415
952
          Assert(!it->second.isNull());
416
952
          child = it->second;
417
        }
418
1342
        childChanged = childChanged || cn != child;
419
1342
        children.push_back(child);
420
      }
421
1453
      if (childChanged)
422
      {
423
383
        ret = nm->mkNode(cur.getKind(), children);
424
      }
425
1453
      visited[cur] = ret;
426
    }
427
3072
  } while (!visit.empty());
428
277
  Assert(visited.find(n) != visited.end());
429
277
  Assert(!visited.find(n)->second.isNull());
430
277
  return visited[n];
431
}
432
433
287
Node SygusRepairConst::getFoQuery(Node body,
434
                                  const std::vector<Node>& candidates,
435
                                  const std::vector<Node>& candidate_skeletons,
436
                                  const std::vector<Node>& sk_vars)
437
{
438
287
  NodeManager* nm = NodeManager::currentNM();
439
287
  Trace("sygus-repair-const") << "  Substitute skeletons..." << std::endl;
440
287
  body = body.substitute(candidates.begin(),
441
                         candidates.end(),
442
                         candidate_skeletons.begin(),
443
                         candidate_skeletons.end());
444
287
  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
445
446
287
  Trace("sygus-repair-const") << "  Unfold the specification..." << std::endl;
447
287
  body = d_tds->evaluateWithUnfolding(body);
448
287
  Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
449
450
287
  Trace("sygus-repair-const") << "  Introduce first-order vars..." << std::endl;
451
689
  for (const Node& v : sk_vars)
452
  {
453
402
    std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
454
402
    if (itf == d_sk_to_fo.end())
455
    {
456
58
      TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
457
58
      Node sk_fov = nm->mkSkolem("k", builtinType);
458
29
      d_sk_to_fo[v] = sk_fov;
459
29
      d_fo_to_sk[sk_fov] = v;
460
58
      Trace("sygus-repair-const-debug")
461
29
          << "Map " << v << " -> " << sk_fov << std::endl;
462
    }
463
  }
464
  // now, we must replace all terms of the form eval( z_i, t1...tn ) with
465
  // a fresh first-order variable w_i, where z_i is a variable introduced in
466
  // the skeleton inference step (z_i is a variable in sk_vars).
467
574
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
468
287
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
469
574
  std::vector<TNode> visit;
470
574
  TNode cur;
471
287
  visit.push_back(body);
472
21390
  do
473
  {
474
21677
    cur = visit.back();
475
21677
    visit.pop_back();
476
21677
    it = visited.find(cur);
477
478
21677
    if (it == visited.end())
479
    {
480
10037
      visited[cur] = Node::null();
481
10037
      if (cur.getKind() == DT_SYGUS_EVAL)
482
      {
483
3806
        Node v = cur[0];
484
1903
        if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
485
        {
486
1903
          std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
487
1903
          Assert(itf != d_sk_to_fo.end());
488
1903
          visited[cur] = itf->second;
489
        }
490
      }
491
10037
      if (visited[cur].isNull())
492
      {
493
8134
        visit.push_back(cur);
494
21390
        for (const Node& cn : cur)
495
        {
496
13256
          visit.push_back(cn);
497
        }
498
      }
499
    }
500
11640
    else if (it->second.isNull())
501
    {
502
16268
      Node ret = cur;
503
8134
      bool childChanged = false;
504
16268
      std::vector<Node> children;
505
8134
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
506
      {
507
240
        children.push_back(cur.getOperator());
508
      }
509
21390
      for (const Node& cn : cur)
510
      {
511
13256
        it = visited.find(cn);
512
13256
        Assert(it != visited.end());
513
13256
        Assert(!it->second.isNull());
514
13256
        childChanged = childChanged || cn != it->second;
515
13256
        children.push_back(it->second);
516
      }
517
8134
      if (childChanged)
518
      {
519
3681
        ret = nm->mkNode(cur.getKind(), children);
520
      }
521
8134
      visited[cur] = ret;
522
    }
523
21677
  } while (!visit.empty());
524
287
  Assert(visited.find(body) != visited.end());
525
287
  Assert(!visited.find(body)->second.isNull());
526
287
  Node fo_body = visited[body];
527
287
  Trace("sygus-repair-const-debug") << "  ...got : " << fo_body << std::endl;
528
574
  return fo_body;
529
}
530
531
170
Node SygusRepairConst::fitToLogic(Node body,
532
                                  LogicInfo& logic,
533
                                  Node n,
534
                                  const std::vector<Node>& candidates,
535
                                  std::vector<Node>& candidate_skeletons,
536
                                  std::vector<Node>& sk_vars,
537
                                  std::map<Node, Node>& sk_vars_to_subs)
538
{
539
340
  std::vector<Node> rm_var;
540
340
  Node exc_var;
541
182
  while (getFitToLogicExcludeVar(logic, n, exc_var))
542
  {
543
170
    if (exc_var.isNull())
544
    {
545
164
      return n;
546
    }
547
12
    Trace("sygus-repair-const") << "...exclude " << exc_var
548
6
                                << " due to logic restrictions." << std::endl;
549
12
    TNode tvar = exc_var;
550
6
    Assert(sk_vars_to_subs.find(exc_var) != sk_vars_to_subs.end());
551
12
    TNode tsubs = sk_vars_to_subs[exc_var];
552
    // revert the substitution
553
12
    for (unsigned i = 0, size = candidate_skeletons.size(); i < size; i++)
554
    {
555
6
      candidate_skeletons[i] = candidate_skeletons[i].substitute(tvar, tsubs);
556
    }
557
    // remove the variable
558
6
    sk_vars_to_subs.erase(exc_var);
559
    std::vector<Node>::iterator it =
560
6
        std::find(sk_vars.begin(), sk_vars.end(), exc_var);
561
6
    Assert(it != sk_vars.end());
562
6
    sk_vars.erase(it);
563
    // reconstruct the query
564
6
    n = getFoQuery(body, candidates, candidate_skeletons, sk_vars);
565
    // reset the exclusion variable
566
6
    exc_var = Node::null();
567
  }
568
6
  return Node::null();
569
}
570
571
176
bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
572
                                               Node n,
573
                                               Node& exvar)
574
{
575
176
  bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear();
576
577
  // should have at least one restriction
578
176
  Assert(restrictLA);
579
580
352
  std::unordered_set<TNode, TNodeHashFunction> visited;
581
176
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
582
352
  std::vector<TNode> visit;
583
352
  TNode cur;
584
176
  visit.push_back(n);
585
7228
  do
586
  {
587
7404
    cur = visit.back();
588
7404
    visit.pop_back();
589
7404
    it = visited.find(cur);
590
591
7404
    if (it == visited.end())
592
    {
593
4834
      visited.insert(cur);
594
4834
      Kind ck = cur.getKind();
595
9668
      bool isArithDivKind = (ck == DIVISION_TOTAL || ck == INTS_DIVISION_TOTAL
596
9668
                             || ck == INTS_MODULUS_TOTAL);
597
4834
      Assert(ck != DIVISION && ck != INTS_DIVISION && ck != INTS_MODULUS);
598
4834
      if (restrictLA && (ck == NONLINEAR_MULT || isArithDivKind))
599
      {
600
30
        for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
601
        {
602
42
          Node ccur = cur[j];
603
24
          std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
604
24
          if (itf != d_fo_to_sk.end())
605
          {
606
6
            if (ck == NONLINEAR_MULT || (isArithDivKind && j == 1))
607
            {
608
6
              exvar = itf->second;
609
6
              return true;
610
            }
611
          }
612
        }
613
6
        return false;
614
      }
615
12176
      for (const Node& ccur : cur)
616
      {
617
7354
        visit.push_back(ccur);
618
      }
619
    }
620
7392
  } while (!visit.empty());
621
622
164
  return true;
623
}
624
625
} /* CVC4::theory::quantifiers namespace */
626
} /* CVC4::theory namespace */
627
27150
} /* CVC4 namespace */