GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_pbe.cpp Lines: 119 119 100.0 %
Date: 2021-03-22 Branches: 223 512 43.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_pbe.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Morgan Deters
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 programming by examples synthesis conjectures
13
 **
14
 **/
15
#include "theory/quantifiers/sygus/sygus_pbe.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/sygus/example_infer.h"
19
#include "theory/quantifiers/sygus/sygus_unif_io.h"
20
#include "theory/quantifiers/sygus/synth_conjecture.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
#include "theory/quantifiers/term_util.h"
23
#include "util/random.h"
24
25
using namespace CVC4;
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
2190
SygusPbe::SygusPbe(QuantifiersEngine* qe,
33
                   QuantifiersInferenceManager& qim,
34
2190
                   SynthConjecture* p)
35
2190
    : SygusModule(qe, qim, p)
36
{
37
2190
  d_true = NodeManager::currentNM()->mkConst(true);
38
2190
  d_false = NodeManager::currentNM()->mkConst(false);
39
2190
  d_is_pbe = false;
40
2190
}
41
42
4376
SygusPbe::~SygusPbe() {}
43
44
383
bool SygusPbe::initialize(Node conj,
45
                          Node n,
46
                          const std::vector<Node>& candidates,
47
                          std::vector<Node>& lemmas)
48
{
49
383
  Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
50
383
  NodeManager* nm = NodeManager::currentNM();
51
52
383
  if (!options::sygusUnifPbe())
53
  {
54
    // we are not doing unification
55
46
    return false;
56
  }
57
58
  // check if all candidates are valid examples
59
337
  ExampleInfer* ei = d_parent->getExampleInfer();
60
337
  d_is_pbe = true;
61
421
  for (const Node& c : candidates)
62
  {
63
    // if it has no examples or the output of the examples is invalid
64
342
    if (ei->getNumExamples(c) == 0 || !ei->hasExamplesOut(c))
65
    {
66
258
      d_is_pbe = false;
67
258
      return false;
68
    }
69
  }
70
163
  for (const Node& c : candidates)
71
  {
72
84
    Assert(ei->hasExamples(c));
73
84
    d_sygus_unif[c].reset(new SygusUnifIo(d_parent));
74
168
    Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
75
84
                       << std::endl;
76
168
    std::map<Node, std::vector<Node>> strategy_lemmas;
77
168
    d_sygus_unif[c]->initializeCandidate(
78
84
        d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
79
84
    Assert(!d_candidate_to_enum[c].empty());
80
168
    Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
81
84
                       << " enumerators for " << c << "..." << std::endl;
82
    // collect list per type of strategy points with strategy lemmas
83
168
    std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
84
181
    for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
85
    {
86
194
      TypeNode tnsp = p.first.getType();
87
97
      tn_to_strategy_pt[tnsp].push_back(p.first);
88
    }
89
    // initialize the enumerators
90
198
    for (const Node& e : d_candidate_to_enum[c])
91
    {
92
228
      TypeNode etn = e.getType();
93
114
      d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL);
94
114
      d_enum_to_candidate[e] = c;
95
228
      TNode te = e;
96
      // initialize static symmetry breaking lemmas for it
97
      // we register only one "master" enumerator per type
98
      // thus, the strategy lemmas (which are for individual strategy points)
99
      // are applicable (disjunctively) to the master enumerator
100
      std::map<TypeNode, std::vector<Node>>::iterator itt =
101
114
          tn_to_strategy_pt.find(etn);
102
114
      if (itt != tn_to_strategy_pt.end())
103
      {
104
126
        std::vector<Node> disj;
105
156
        for (const Node& sp : itt->second)
106
        {
107
          std::map<Node, std::vector<Node>>::iterator itsl =
108
93
              strategy_lemmas.find(sp);
109
93
          Assert(itsl != strategy_lemmas.end());
110
93
          if (!itsl->second.empty())
111
          {
112
186
            TNode tsp = sp;
113
174
            Node lem = itsl->second.size() == 1 ? itsl->second[0]
114
267
                                                : nm->mkNode(AND, itsl->second);
115
93
            if (tsp != te)
116
            {
117
30
              lem = lem.substitute(tsp, te);
118
            }
119
93
            if (std::find(disj.begin(), disj.end(), lem) == disj.end())
120
            {
121
67
              disj.push_back(lem);
122
            }
123
          }
124
        }
125
        // add its active guard
126
126
        Node ag = d_tds->getActiveGuardForEnumerator(e);
127
63
        Assert(!ag.isNull());
128
63
        disj.push_back(ag.negate());
129
126
        Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
130
        // Apply extended rewriting on the lemma. This helps utilities like
131
        // SygusEnumerator more easily recognize the shape of this lemma, e.g.
132
        // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
133
63
        lem = d_tds->getExtRewriter()->extendedRewrite(lem);
134
126
        Trace("sygus-pbe") << "  static redundant op lemma : " << lem
135
63
                           << std::endl;
136
        // Register as a symmetry breaking lemma with the term database.
137
        // This will either be processed via a lemma on the output channel
138
        // of the sygus extension of the datatypes solver, or internally
139
        // encoded as a constraint to an active enumerator.
140
63
        d_tds->registerSymBreakLemma(e, lem, etn, 0, false);
141
      }
142
    }
143
  }
144
79
  return true;
145
}
146
147
// ------------------------------------------- solution construction from enumeration
148
149
7064
void SygusPbe::getTermList(const std::vector<Node>& candidates,
150
                           std::vector<Node>& terms)
151
{
152
14275
  for( unsigned i=0; i<candidates.size(); i++ ){
153
14422
    Node v = candidates[i];
154
    std::map<Node, std::vector<Node> >::iterator it =
155
7211
        d_candidate_to_enum.find(v);
156
7211
    if (it != d_candidate_to_enum.end())
157
    {
158
7211
      terms.insert(terms.end(), it->second.begin(), it->second.end());
159
    }
160
  }
161
7064
}
162
163
15134
bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
164
165
891
bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
166
                                   const std::vector<Node>& enum_values,
167
                                   const std::vector<Node>& candidates,
168
                                   std::vector<Node>& candidate_values,
169
                                   std::vector<Node>& lems)
170
{
171
891
  Assert(enums.size() == enum_values.size());
172
891
  if( !enums.empty() ){
173
891
    unsigned min_term_size = 0;
174
891
    Trace("sygus-pbe-enum") << "Register new enumerated values : " << std::endl;
175
1782
    std::vector<unsigned> szs;
176
2138
    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
177
    {
178
1247
      Trace("sygus-pbe-enum") << "  " << enums[i] << " -> ";
179
1247
      TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]);
180
1247
      Trace("sygus-pbe-enum") << std::endl;
181
1247
      if (!enum_values[i].isNull())
182
      {
183
1006
        unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
184
1006
        szs.push_back(sz);
185
1006
        if (i == 0 || sz < min_term_size)
186
        {
187
838
          min_term_size = sz;
188
        }
189
      }
190
      else
191
      {
192
241
        szs.push_back(0);
193
      }
194
    }
195
    // Assume two enumerators of types T1 and T2.
196
    // If options::sygusPbeMultiFair() is true,
197
    // we ensure that all values of type T1 and size n are enumerated before
198
    // any term of type T2 of size n+d, and vice versa, where d is
199
    // set by options::sygusPbeMultiFairDiff(). If d is zero, then our
200
    // enumeration is such that all terms of T1 or T2 of size n are considered
201
    // before any term of size n+1.
202
1782
    int diffAllow = options::sygusPbeMultiFairDiff();
203
1782
    std::vector<unsigned> enum_consider;
204
2138
    for (unsigned i = 0, esize = enums.size(); i < esize; i++)
205
    {
206
1247
      if (!enum_values[i].isNull())
207
      {
208
1006
        Assert(szs[i] >= min_term_size);
209
1006
        int diff = szs[i] - min_term_size;
210
1006
        if (!options::sygusPbeMultiFair() || diff <= diffAllow)
211
        {
212
1006
          enum_consider.push_back(i);
213
        }
214
      }
215
    }
216
217
    // only consider the enumerators that are at minimum size (for fairness)
218
891
    Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl;
219
891
    NodeManager* nm = NodeManager::currentNM();
220
1897
    for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; i++)
221
    {
222
1006
      unsigned j = enum_consider[i];
223
2012
      Node e = enums[j];
224
2012
      Node v = enum_values[j];
225
1006
      Assert(d_enum_to_candidate.find(e) != d_enum_to_candidate.end());
226
2012
      Node c = d_enum_to_candidate[e];
227
2012
      std::vector<Node> enum_lems;
228
1006
      d_sygus_unif[c]->notifyEnumeration(e, v, enum_lems);
229
1006
      if (!enum_lems.empty())
230
      {
231
        // the lemmas must be guarded by the active guard of the enumerator
232
28
        Node g = d_tds->getActiveGuardForEnumerator(e);
233
14
        Assert(!g.isNull());
234
28
        for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
235
        {
236
14
          enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]);
237
        }
238
14
        lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
239
      }
240
    }
241
  }
242
984
  for( unsigned i=0; i<candidates.size(); i++ ){
243
999
    Node c = candidates[i];
244
    //build decision tree for candidate
245
999
    std::vector<Node> sol;
246
906
    if (d_sygus_unif[c]->constructSolution(sol, lems))
247
    {
248
93
      Assert(sol.size() == 1);
249
93
      candidate_values.push_back(sol[0]);
250
    }
251
    else
252
    {
253
813
      return false;
254
    }
255
  }
256
78
  return true;
257
}
258
259
}
260
}
261
26676
}