GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_eval_unfold.cpp Lines: 180 185 97.3 %
Date: 2021-03-22 Branches: 392 934 42.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_eval_unfold.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of sygus_eval_unfold
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
16
17
#include "expr/dtype_cons.h"
18
#include "expr/sygus_datatype.h"
19
#include "options/quantifiers_options.h"
20
#include "theory/datatypes/sygus_datatype_utils.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
#include "theory/rewriter.h"
23
24
using namespace std;
25
using namespace CVC4::kind;
26
using namespace CVC4::context;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
2190
SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
33
34
297479
void SygusEvalUnfold::registerEvalTerm(Node n)
35
{
36
297479
  Assert(options::sygusEvalUnfold());
37
  // is this a sygus evaluation function application?
38
297479
  if (n.getKind() != DT_SYGUS_EVAL)
39
  {
40
587151
    return;
41
  }
42
5745
  if (d_eval_processed.find(n) != d_eval_processed.end())
43
  {
44
3683
    return;
45
  }
46
4124
  Trace("sygus-eval-unfold")
47
2062
      << "SygusEvalUnfold: register eval term : " << n << std::endl;
48
2062
  d_eval_processed.insert(n);
49
4124
  TypeNode tn = n[0].getType();
50
  // since n[0] is an evaluation head, we know tn is a sygus datatype
51
2062
  Assert(tn.isDatatype());
52
2062
  const DType& dt = tn.getDType();
53
2062
  Assert(dt.isSygus());
54
2062
  if (n[0].getKind() == APPLY_CONSTRUCTOR)
55
  {
56
    // constructors should be unfolded and reduced already
57
    Assert(false);
58
    return;
59
  }
60
  // register this evaluation term with its head
61
2062
  d_evals[n[0]].push_back(n);
62
4124
  Node var_list = dt.getSygusVarList();
63
2062
  d_eval_args[n[0]].push_back(std::vector<Node>());
64
8391
  for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
65
  {
66
6329
    d_eval_args[n[0]].back().push_back(n[j]);
67
  }
68
4124
  Node a = TermDbSygus::getAnchor(n[0]);
69
2062
  d_subterms[a].insert(n[0]);
70
}
71
72
32299
void SygusEvalUnfold::registerModelValue(Node a,
73
                                         Node v,
74
                                         std::vector<Node>& terms,
75
                                         std::vector<Node>& vals,
76
                                         std::vector<Node>& exps)
77
{
78
  std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator its =
79
32299
      d_subterms.find(a);
80
32299
  if (its == d_subterms.end())
81
  {
82
6775
    return;
83
  }
84
25524
  NodeManager* nm = NodeManager::currentNM();
85
25524
  SygusExplain* sy_exp = d_tds->getExplain();
86
51048
  Trace("sygus-eval-unfold")
87
51048
      << "SygusEvalUnfold: " << a << ", has " << its->second.size()
88
25524
      << " registered subterms." << std::endl;
89
56916
  for (const Node& n : its->second)
90
  {
91
31392
    Trace("sygus-eval-unfold-debug") << "...process : " << n << std::endl;
92
    std::map<Node, std::vector<std::vector<Node> > >::iterator it =
93
31392
        d_eval_args.find(n);
94
31392
    if (it != d_eval_args.end() && !it->second.empty())
95
    {
96
62784
      TNode at = a;
97
62784
      TNode vt = v;
98
62784
      Node vn = n.substitute(at, vt);
99
31392
      vn = Rewriter::rewrite(vn);
100
31392
      unsigned start = d_node_mv_args_proc[n][vn];
101
      // get explanation in terms of testers
102
62784
      std::vector<Node> antec_exp;
103
31392
      sy_exp->getExplanationForEquality(n, vn, antec_exp);
104
      Node antec =
105
62784
          antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
106
      // Node antec = n.eqNode( vn );
107
62784
      TypeNode tn = n.getType();
108
      // Check if the sygus type has any symbolic constructors. This will
109
      // impact how the unfolding is computed below.
110
31392
      SygusTypeInfo& sti = d_tds->getTypeInfo(tn);
111
31392
      bool hasSymCons = sti.hasSubtermSymbolicCons();
112
      // n occurs as an evaluation head, thus it has sygus datatype type
113
31392
      Assert(tn.isDatatype());
114
31392
      const DType& dt = tn.getDType();
115
31392
      Assert(dt.isSygus());
116
62784
      Trace("sygus-eval-unfold")
117
31392
          << "SygusEvalUnfold: Register model value : " << vn << " for " << n
118
31392
          << std::endl;
119
31392
      unsigned curr_size = it->second.size();
120
62784
      Trace("sygus-eval-unfold")
121
31392
          << "...it has " << curr_size << " evaluations, already processed "
122
31392
          << start << "." << std::endl;
123
62784
      Node bTerm = d_tds->sygusToBuiltin(vn, tn);
124
31392
      Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
125
62784
      std::vector<Node> vars;
126
62784
      Node var_list = dt.getSygusVarList();
127
602929
      for (const Node& var : var_list)
128
      {
129
571537
        vars.push_back(var);
130
      }
131
      // evaluation children
132
62784
      std::vector<Node> eval_children;
133
31392
      eval_children.push_back(n);
134
      // for each evaluation
135
47131
      for (unsigned i = start; i < curr_size; i++)
136
      {
137
31478
        Node res;
138
31478
        Node expn;
139
        // should we unfold?
140
15739
        bool do_unfold = false;
141
31478
        if (options::sygusEvalUnfoldBool())
142
        {
143
31478
          Node bTermUse = bTerm;
144
15739
          if (bTerm.getKind() == APPLY_UF)
145
          {
146
            // if the builtin term is non-beta-reduced application of lambda,
147
            // we look at the body of the lambda.
148
16
            Node bTermOp = bTerm.getOperator();
149
8
            if (bTermOp.getKind() == LAMBDA)
150
            {
151
              bTermUse = bTermOp[0];
152
            }
153
          }
154
15739
          if (bTermUse.getKind() == ITE || bTermUse.getType().isBoolean())
155
          {
156
3483
            do_unfold = true;
157
          }
158
        }
159
15739
        if (do_unfold || hasSymCons)
160
        {
161
          // note that this is replicated for different values
162
8774
          std::map<Node, Node> vtm;
163
8774
          std::vector<Node> exp;
164
4387
          vtm[n] = vn;
165
4387
          eval_children.insert(
166
8774
              eval_children.end(), it->second[i].begin(), it->second[i].end());
167
8774
          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
168
4387
          eval_children.resize(1);
169
          // If we explicitly asked to unfold, we use single step, otherwise
170
          // we use multi step.
171
4387
          res = unfold(eval_fun, vtm, exp, true, !do_unfold);
172
4387
          Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl;
173
8774
          expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
174
        }
175
        else
176
        {
177
22704
          EvalSygusInvarianceTest esit;
178
11352
          eval_children.insert(
179
22704
              eval_children.end(), it->second[i].begin(), it->second[i].end());
180
22704
          Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
181
11352
          eval_children[0] = vn;
182
22704
          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
183
11352
          res = d_tds->evaluateWithUnfolding(eval_fun);
184
22704
          Trace("sygus-eval-unfold")
185
11352
              << "Evaluate with unfolding returns " << res << std::endl;
186
11352
          esit.init(conj, n, res);
187
11352
          eval_children.resize(1);
188
11352
          eval_children[0] = n;
189
190
          // evaluate with minimal explanation
191
22704
          std::vector<Node> mexp;
192
11352
          sy_exp->getExplanationFor(n, vn, mexp, esit);
193
11352
          Assert(!mexp.empty());
194
11352
          expn = mexp.size() == 1 ? mexp[0] : nm->mkNode(AND, mexp);
195
        }
196
15739
        Assert(!res.isNull());
197
15739
        terms.push_back(d_evals[n][i]);
198
15739
        vals.push_back(res);
199
15739
        exps.push_back(expn);
200
31478
        Trace("sygus-eval-unfold")
201
15739
            << "Conclude : " << d_evals[n][i] << " == " << res << std::endl;
202
15739
        Trace("sygus-eval-unfold") << "   from " << expn << std::endl;
203
      }
204
31392
      d_node_mv_args_proc[n][vn] = curr_size;
205
    }
206
  }
207
}
208
209
72538
Node SygusEvalUnfold::unfold(Node en,
210
                             std::map<Node, Node>& vtm,
211
                             std::vector<Node>& exp,
212
                             bool track_exp,
213
                             bool doRec)
214
{
215
72538
  if (en.getKind() != DT_SYGUS_EVAL)
216
  {
217
    Assert(en.isConst());
218
    return en;
219
  }
220
145076
  Trace("sygus-eval-unfold-debug")
221
72538
      << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is "
222
72538
      << doRec << std::endl;
223
145076
  Node ev = en[0];
224
72538
  if (track_exp)
225
  {
226
6779
    std::map<Node, Node>::iterator itv = vtm.find(en[0]);
227
6779
    Assert(itv != vtm.end());
228
6779
    if (itv != vtm.end())
229
    {
230
6779
      ev = itv->second;
231
    }
232
6779
    Assert(en[0].getType() == ev.getType());
233
6779
    Assert(ev.isConst());
234
  }
235
145076
  Trace("sygus-eval-unfold-debug")
236
72538
      << "Unfold model value is : " << ev << std::endl;
237
72538
  AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR);
238
145076
  std::vector<Node> args;
239
232326
  for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
240
  {
241
159788
    args.push_back(en[i]);
242
  }
243
244
145076
  TypeNode headType = en[0].getType();
245
72538
  NodeManager* nm = NodeManager::currentNM();
246
72538
  const DType& dt = headType.getDType();
247
72538
  unsigned i = datatypes::utils::indexOf(ev.getOperator());
248
72538
  if (track_exp)
249
  {
250
    // explanation
251
13558
    Node ee = nm->mkNode(APPLY_TESTER, dt[i].getTester(), en[0]);
252
6779
    if (std::find(exp.begin(), exp.end(), ee) == exp.end())
253
    {
254
6779
      exp.push_back(ee);
255
    }
256
  }
257
  // if we are a symbolic constructor, unfolding returns the subterm itself
258
145076
  Node sop = dt[i].getSygusOp();
259
72538
  if (sop.getAttribute(SygusAnyConstAttribute()))
260
  {
261
1896
    Trace("sygus-eval-unfold-debug")
262
948
        << "...it is an any-constant constructor" << std::endl;
263
948
    Assert(dt[i].getNumArgs() == 1);
264
    // If the argument to evaluate is itself concrete, then we use its
265
    // argument; otherwise we return its selector.
266
948
    if (en[0].getKind() == APPLY_CONSTRUCTOR)
267
    {
268
4
      Trace("sygus-eval-unfold-debug")
269
2
          << "...return (from constructor) " << en[0][0] << std::endl;
270
2
      return en[0][0];
271
    }
272
    else
273
    {
274
      Node ret = nm->mkNode(
275
1892
          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
276
1892
      Trace("sygus-eval-unfold-debug")
277
946
          << "...return (from constructor) " << ret << std::endl;
278
946
      return ret;
279
    }
280
  }
281
282
71590
  Assert(!dt.isParametric());
283
143180
  std::map<int, Node> pre;
284
214174
  for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
285
  {
286
285168
    std::vector<Node> cc;
287
285168
    Node s;
288
    // get the j^th subfield of en
289
142584
    if (en[0].getKind() == APPLY_CONSTRUCTOR)
290
    {
291
      // if it is a concrete constructor application, as an optimization,
292
      // just return the argument
293
133211
      s = en[0][j];
294
    }
295
    else
296
    {
297
28119
      s = nm->mkNode(
298
18746
          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
299
    }
300
142584
    cc.push_back(s);
301
142584
    if (track_exp)
302
    {
303
      // update vtm map
304
9373
      vtm[s] = ev[j];
305
    }
306
142584
    cc.insert(cc.end(), args.begin(), args.end());
307
285168
    Node argj = nm->mkNode(DT_SYGUS_EVAL, cc);
308
142584
    if (doRec)
309
    {
310
2392
      Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl;
311
      // evaluate recursively
312
2392
      argj = unfold(argj, vtm, exp, track_exp, doRec);
313
    }
314
142584
    pre[j] = argj;
315
  }
316
143180
  Node ret = d_tds->mkGeneric(dt, i, pre);
317
  // apply the appropriate substitution to ret
318
71590
  ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
319
143180
  Trace("sygus-eval-unfold-debug")
320
71590
      << "Applied sygus args : " << ret << std::endl;
321
  // rewrite
322
71590
  ret = Rewriter::rewrite(ret);
323
71590
  Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl;
324
71590
  return ret;
325
}
326
327
65759
Node SygusEvalUnfold::unfold(Node en)
328
{
329
131518
  std::map<Node, Node> vtm;
330
131518
  std::vector<Node> exp;
331
131518
  return unfold(en, vtm, exp, false, false);
332
}
333
334
}  // namespace quantifiers
335
}  // namespace theory
336
42415
}  // namespace CVC4