GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/template_infer.cpp Lines: 93 95 97.9 %
Date: 2021-03-22 Branches: 239 538 44.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file template_infer.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 utility for processing single invocation synthesis conjectures
13
 **
14
 **/
15
#include "theory/quantifiers/sygus/template_infer.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
19
#include "theory/quantifiers/sygus/sygus_utils.h"
20
#include "theory/quantifiers/term_util.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
506
void SygusTemplateInfer::initialize(Node q)
29
{
30
506
  Assert(d_quant.isNull());
31
506
  Assert(q.getKind() == FORALL);
32
506
  d_quant = q;
33
  // We are processing without single invocation techniques, now check if
34
  // we should fix an invariant template (post-condition strengthening or
35
  // pre-condition weakening).
36
506
  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
37
506
  if (tmode != options::SygusInvTemplMode::NONE)
38
  {
39
    // currently only works for single predicate synthesis
40
472
    if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
41
    {
42
357
      tmode = options::SygusInvTemplMode::NONE;
43
    }
44
230
    else if (!options::sygusInvTemplWhenSyntax())
45
    {
46
      // only use invariant templates if no syntactic restrictions
47
115
      if (CegGrammarConstructor::hasSyntaxRestrictions(q))
48
      {
49
58
        tmode = options::SygusInvTemplMode::NONE;
50
      }
51
    }
52
  }
53
54
506
  if (tmode == options::SygusInvTemplMode::NONE)
55
  {
56
    // not processing invariant templates
57
908
    return;
58
  }
59
60
104
  Node qq;
61
57
  if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL)
62
  {
63
47
    qq = q[1][0][1];
64
  }
65
  else
66
  {
67
10
    qq = TermUtil::simpleNegate(q[1]);
68
  }
69
57
  if (qq.isConst())
70
  {
71
    // trivial, do not use transition inference
72
3
    return;
73
  }
74
75
  // if we are doing invariant templates, then construct the template
76
54
  Trace("sygus-si") << "- Do transition inference..." << std::endl;
77
54
  d_ti.process(qq, q[0][0]);
78
54
  Trace("cegqi-inv") << std::endl;
79
101
  Node prog = d_ti.getFunction();
80
54
  if (!d_ti.isComplete())
81
  {
82
    // the invariant could not be inferred
83
7
    return;
84
  }
85
47
  Assert(prog == q[0][0]);
86
47
  NodeManager* nm = NodeManager::currentNM();
87
  // map the program back via non-single invocation map
88
94
  std::vector<Node> prog_templ_vars;
89
47
  d_ti.getVariables(prog_templ_vars);
90
47
  d_trans_pre[prog] = d_ti.getPreCondition();
91
47
  d_trans_post[prog] = d_ti.getPostCondition();
92
47
  Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
93
47
  Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
94
95
  // construct template argument
96
94
  TypeNode atn = prog.getType();
97
47
  if (atn.isFunction())
98
  {
99
47
    atn = atn.getRangeType();
100
  }
101
47
  d_templ_arg[prog] = nm->mkSkolem("I", atn);
102
103
  // construct template
104
94
  Node templ;
105
94
  if (options::sygusInvAutoUnfold())
106
  {
107
47
    if (d_ti.isComplete())
108
    {
109
94
      Trace("cegqi-inv-auto-unfold")
110
47
          << "Automatic deterministic unfolding... " << std::endl;
111
      // auto-unfold
112
94
      DetTrace dt;
113
47
      int init_dt = d_ti.initializeTrace(dt);
114
47
      if (init_dt == 0)
115
      {
116
10
        Trace("cegqi-inv-auto-unfold") << "  Init : ";
117
10
        dt.print("cegqi-inv-auto-unfold");
118
10
        Trace("cegqi-inv-auto-unfold") << std::endl;
119
10
        unsigned counter = 0;
120
10
        unsigned status = 0;
121
1068
        while (counter < 100 && status == 0)
122
        {
123
529
          status = d_ti.incrementTrace(dt);
124
529
          counter++;
125
529
          Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
126
529
          dt.print("cegqi-inv-auto-unfold");
127
1058
          Trace("cegqi-inv-auto-unfold")
128
529
              << "...status = " << status << std::endl;
129
        }
130
10
        if (status == 1)
131
        {
132
          // we have a trivial invariant
133
5
          templ = d_ti.constructFormulaTrace(dt);
134
10
          Trace("cegqi-inv") << "By finite deterministic terminating trace, a "
135
5
                                "solution invariant is : "
136
5
                             << std::endl;
137
5
          Trace("cegqi-inv") << "   " << templ << std::endl;
138
          // this should be unnecessary
139
5
          templ = nm->mkNode(AND, templ, d_templ_arg[prog]);
140
        }
141
      }
142
      else
143
      {
144
37
        Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
145
      }
146
    }
147
  }
148
94
  Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ
149
47
                     << std::endl;
150
47
  if (templ.isNull())
151
  {
152
42
    if (tmode == options::SygusInvTemplMode::PRE)
153
    {
154
      templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]);
155
    }
156
    else
157
    {
158
42
      Assert(tmode == options::SygusInvTemplMode::POST);
159
42
      templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]);
160
    }
161
  }
162
94
  Trace("cegqi-inv") << "       template (pre-substitution) : " << templ
163
47
                     << std::endl;
164
47
  Assert(!templ.isNull());
165
166
  // get the variables
167
94
  Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(prog);
168
47
  if (!sfvl.isNull())
169
  {
170
94
    std::vector<Node> prog_vars(sfvl.begin(), sfvl.end());
171
    // subsitute the template arguments
172
94
    Trace("cegqi-inv") << "vars : " << prog_templ_vars << " " << prog_vars
173
47
                       << std::endl;
174
47
    Assert(prog_templ_vars.size() == prog_vars.size());
175
47
    templ = templ.substitute(prog_templ_vars.begin(),
176
                             prog_templ_vars.end(),
177
                             prog_vars.begin(),
178
                             prog_vars.end());
179
  }
180
47
  Trace("cegqi-inv") << "       template : " << templ << std::endl;
181
47
  d_templ[prog] = templ;
182
}
183
184
2505
Node SygusTemplateInfer::getTemplate(Node prog) const
185
{
186
2505
  std::map<Node, Node>::const_iterator tmpl = d_templ.find(prog);
187
2505
  if (tmpl != d_templ.end())
188
  {
189
64
    return tmpl->second;
190
  }
191
2441
  return Node::null();
192
}
193
194
64
Node SygusTemplateInfer::getTemplateArg(Node prog) const
195
{
196
64
  std::map<Node, Node>::const_iterator tmpla = d_templ_arg.find(prog);
197
64
  if (tmpla != d_templ_arg.end())
198
  {
199
64
    return tmpla->second;
200
  }
201
  return Node::null();
202
}
203
204
}  // namespace quantifiers
205
}  // namespace theory
206
26838
}  // namespace CVC4