GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/synth_engine.cpp Lines: 134 140 95.7 %
Date: 2021-03-22 Branches: 220 408 53.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file synth_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
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 the quantifiers module for managing all approaches
13
 ** to synthesis, in particular, those described in Reynolds et al CAV 2015.
14
 **
15
 **/
16
#include "theory/quantifiers/sygus/synth_engine.h"
17
18
#include "expr/node_algorithm.h"
19
#include "options/quantifiers_options.h"
20
#include "theory/quantifiers/quantifiers_attributes.h"
21
#include "theory/quantifiers/sygus/term_database_sygus.h"
22
#include "theory/quantifiers/term_util.h"
23
#include "theory/quantifiers_engine.h"
24
25
using namespace CVC4::kind;
26
using namespace std;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
2190
SynthEngine::SynthEngine(QuantifiersEngine* qe,
33
                         QuantifiersState& qs,
34
                         QuantifiersInferenceManager& qim,
35
2190
                         QuantifiersRegistry& qr)
36
    : QuantifiersModule(qs, qim, qr, qe),
37
2190
      d_tds(qe->getTermDatabaseSygus()),
38
      d_conj(nullptr),
39
4380
      d_sqp(qe)
40
{
41
4380
  d_conjs.push_back(std::unique_ptr<SynthConjecture>(
42
2190
      new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics)));
43
2190
  d_conj = d_conjs.back().get();
44
2190
}
45
46
4376
SynthEngine::~SynthEngine() {}
47
48
2156
void SynthEngine::presolve()
49
{
50
2156
  Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
51
4312
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
52
  {
53
2156
    d_conjs[i]->presolve();
54
  }
55
2156
  Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
56
2156
}
57
58
20293
bool SynthEngine::needsCheck(Theory::Effort e)
59
{
60
20293
  return e >= Theory::EFFORT_LAST_CALL;
61
}
62
63
8967
QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
64
{
65
8967
  return QEFFORT_MODEL;
66
}
67
68
29390
void SynthEngine::check(Theory::Effort e, QEffort quant_e)
69
{
70
  // are we at the proper effort level?
71
29390
  if (quant_e != QEFFORT_MODEL)
72
  {
73
41696
    return;
74
  }
75
76
  // if we are waiting to assign the conjecture, do it now
77
8545
  bool assigned = !d_waiting_conj.empty();
78
8565
  while (!d_waiting_conj.empty())
79
  {
80
20
    Node q = d_waiting_conj.back();
81
10
    d_waiting_conj.pop_back();
82
20
    Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
83
10
                          << std::endl;
84
10
    assignConjecture(q);
85
  }
86
8545
  if (assigned)
87
  {
88
    // assign conjecture always uses the output channel, either by reducing a
89
    // quantified formula to another, or adding initial lemmas during
90
    // SynthConjecture::assign. Thus, we return here and re-check.
91
6
    return;
92
  }
93
94
17078
  Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
95
8539
                        << std::endl;
96
8539
  Trace("sygus-engine-debug") << std::endl;
97
8539
  Valuation& valuation = d_qstate.getValuation();
98
17078
  std::vector<SynthConjecture*> activeCheckConj;
99
17078
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
100
  {
101
8539
    SynthConjecture* sc = d_conjs[i].get();
102
8539
    bool active = false;
103
    bool value;
104
8539
    if (valuation.hasSatValue(sc->getConjecture(), value))
105
    {
106
8489
      active = value;
107
    }
108
    else
109
    {
110
100
      Trace("sygus-engine-debug") << "...no value for quantified formula."
111
50
                                  << std::endl;
112
    }
113
17078
    Trace("sygus-engine-debug")
114
8539
        << "Current conjecture status : active : " << active << std::endl;
115
8539
    if (active && sc->needsCheck())
116
    {
117
8477
      activeCheckConj.push_back(sc);
118
    }
119
  }
120
17078
  std::vector<SynthConjecture*> acnext;
121
47866
  do
122
  {
123
112810
    Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
124
56405
                                << " active conjectures..." << std::endl;
125
112736
    for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
126
    {
127
56343
      SynthConjecture* sc = activeCheckConj[i];
128
56343
      if (!checkConjecture(sc))
129
      {
130
49214
        if (!sc->needsRefinement())
131
        {
132
49214
          acnext.push_back(sc);
133
        }
134
      }
135
    }
136
56393
    activeCheckConj.clear();
137
56393
    activeCheckConj = acnext;
138
56393
    acnext.clear();
139
56393
  } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
140
17054
  Trace("sygus-engine")
141
8527
      << "Finished Counterexample Guided Instantiation engine." << std::endl;
142
}
143
144
510
void SynthEngine::assignConjecture(Node q)
145
{
146
510
  Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
147
1544
  if (options::sygusQePreproc())
148
  {
149
16
    Node lem = d_sqp.preprocess(q);
150
10
    if (!lem.isNull())
151
    {
152
8
      Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
153
4
                           << std::endl;
154
4
      d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
155
      // we've reduced the original to a preprocessed version, return
156
4
      return;
157
    }
158
  }
159
  // allocate a new synthesis conjecture if not assigned
160
506
  if (d_conjs.back()->isAssigned())
161
  {
162
    d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
163
        d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics)));
164
  }
165
506
  d_conjs.back()->assign(q);
166
}
167
168
1148
void SynthEngine::checkOwnership(Node q)
169
{
170
  // take ownership of quantified formulas with sygus attribute, and function
171
  // definitions when options::sygusRecFun is true.
172
1148
  QuantAttributes& qa = d_qreg.getQuantAttributes();
173
1148
  if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
174
  {
175
551
    d_qreg.setOwner(q, this, 2);
176
  }
177
1148
}
178
179
1148
void SynthEngine::registerQuantifier(Node q)
180
{
181
2296
  Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
182
1148
                       << std::endl;
183
1148
  if (d_qreg.getOwner(q) != this)
184
  {
185
597
    return;
186
  }
187
551
  if (d_qreg.getQuantAttributes().isFunDef(q))
188
  {
189
39
    Assert(options::sygusRecFun());
190
    // If it is a recursive function definition, add it to the function
191
    // definition evaluator class.
192
39
    Trace("cegqi") << "Registering function definition : " << q << "\n";
193
39
    FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
194
39
    fde->assertDefinition(q);
195
39
    return;
196
  }
197
512
  Trace("cegqi") << "Register conjecture : " << q << std::endl;
198
512
  if (options::sygusQePreproc())
199
  {
200
12
    d_waiting_conj.push_back(q);
201
  }
202
  else
203
  {
204
    // assign it now
205
500
    assignConjecture(q);
206
  }
207
}
208
209
56343
bool SynthEngine::checkConjecture(SynthConjecture* conj)
210
{
211
56343
  if (Trace.isOn("sygus-engine-debug"))
212
  {
213
    conj->debugPrint("sygus-engine-debug");
214
    Trace("sygus-engine-debug") << std::endl;
215
  }
216
217
56343
  if (!conj->needsRefinement())
218
  {
219
56333
    Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
220
112666
    Trace("sygus-engine-debug")
221
56333
        << "  *** Check candidate phase..." << std::endl;
222
57008
    std::vector<Node> cclems;
223
56333
    bool ret = conj->doCheck(cclems);
224
56321
    bool addedLemma = false;
225
76212
    for (const Node& lem : cclems)
226
    {
227
19891
      if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
228
      {
229
17426
        ++(d_statistics.d_cegqi_lemmas_ce);
230
17426
        addedLemma = true;
231
      }
232
      else
233
      {
234
        // this may happen if we eagerly unfold, simplify to true
235
4930
        Trace("sygus-engine-debug")
236
2465
            << "  ...FAILED to add candidate!" << std::endl;
237
      }
238
    }
239
56321
    if (addedLemma)
240
    {
241
7612
      Trace("sygus-engine-debug")
242
3806
          << "  ...check for counterexample." << std::endl;
243
3806
      return true;
244
    }
245
52515
    if (!conj->needsRefinement())
246
    {
247
51852
      return ret;
248
    }
249
    // otherwise, immediately go to refine candidate
250
  }
251
673
  Trace("sygus-engine-debug") << "  *** Refine candidate phase..." << std::endl;
252
673
  return conj->doRefine();
253
}
254
255
4
void SynthEngine::printSynthSolution(std::ostream& out)
256
{
257
4
  Assert(!d_conjs.empty());
258
8
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
259
  {
260
4
    if (d_conjs[i]->isAssigned())
261
    {
262
4
      d_conjs[i]->printSynthSolution(out);
263
    }
264
  }
265
4
}
266
267
250
bool SynthEngine::getSynthSolutions(
268
    std::map<Node, std::map<Node, Node> >& sol_map)
269
{
270
250
  bool ret = true;
271
500
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
272
  {
273
250
    if (d_conjs[i]->isAssigned())
274
    {
275
246
      if (!d_conjs[i]->getSynthSolutions(sol_map))
276
      {
277
        // if one conjecture fails, we fail overall
278
        ret = false;
279
        break;
280
      }
281
    }
282
  }
283
250
  return ret;
284
}
285
286
6353
void SynthEngine::preregisterAssertion(Node n)
287
{
288
  // check if it sygus conjecture
289
6353
  if (QuantAttributes::checkSygusConjecture(n))
290
  {
291
    // this is a sygus conjecture
292
508
    Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
293
508
    d_conj->preregisterConjecture(n);
294
  }
295
6353
}
296
297
}  // namespace quantifiers
298
}  // namespace theory
299
26676
} /* namespace CVC4 */