GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/sygus_solver.cpp Lines: 183 210 87.1 %
Date: 2021-03-22 Branches: 331 740 44.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_solver.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 The solver for sygus queries
13
 **/
14
15
#include "smt/sygus_solver.h"
16
17
#include "expr/dtype.h"
18
#include "options/quantifiers_options.h"
19
#include "options/smt_options.h"
20
#include "printer/printer.h"
21
#include "smt/dump.h"
22
#include "smt/preprocessor.h"
23
#include "smt/smt_solver.h"
24
#include "theory/quantifiers/quantifiers_attributes.h"
25
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
26
#include "theory/quantifiers/sygus/sygus_utils.h"
27
#include "theory/quantifiers_engine.h"
28
#include "theory/smt_engine_subsolver.h"
29
30
using namespace CVC4::theory;
31
using namespace CVC4::kind;
32
33
namespace CVC4 {
34
namespace smt {
35
36
9619
SygusSolver::SygusSolver(SmtSolver& sms,
37
                         Preprocessor& pp,
38
                         context::UserContext* u,
39
9619
                         OutputManager& outMgr)
40
    : d_smtSolver(sms),
41
      d_pp(pp),
42
      d_sygusConjectureStale(u, true),
43
9619
      d_outMgr(outMgr)
44
{
45
9619
}
46
47
9598
SygusSolver::~SygusSolver() {}
48
49
683
void SygusSolver::declareSygusVar(Node var)
50
{
51
1366
  Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
52
683
               << var.getType() << "\n";
53
683
  d_sygusVars.push_back(var);
54
  // don't need to set that the conjecture is stale
55
683
}
56
57
575
void SygusSolver::declareSynthFun(Node fn,
58
                                  TypeNode sygusType,
59
                                  bool isInv,
60
                                  const std::vector<Node>& vars)
61
{
62
575
  Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
63
575
  NodeManager* nm = NodeManager::currentNM();
64
575
  d_sygusFunSymbols.push_back(fn);
65
575
  if (!vars.empty())
66
  {
67
1012
    Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
68
    // use an attribute to mark its bound variable list
69
    SygusSynthFunVarListAttribute ssfvla;
70
506
    fn.setAttribute(ssfvla, bvl);
71
  }
72
  // whether sygus type encodes syntax restrictions
73
1725
  if (!sygusType.isNull() && sygusType.isDatatype()
74
865
      && sygusType.getDType().isSygus())
75
  {
76
580
    Node sym = nm->mkBoundVar("sfproxy", sygusType);
77
    // use an attribute to mark its grammar
78
    SygusSynthGrammarAttribute ssfga;
79
290
    fn.setAttribute(ssfga, sym);
80
  }
81
82
  // sygus conjecture is now stale
83
575
  setSygusConjectureStale();
84
575
}
85
86
1201
void SygusSolver::assertSygusConstraint(Node constraint)
87
{
88
1201
  Trace("smt") << "SygusSolver::assertSygusConstrant: " << constraint << "\n";
89
1201
  d_sygusConstraints.push_back(constraint);
90
91
  // sygus conjecture is now stale
92
1201
  setSygusConjectureStale();
93
1201
}
94
95
31
void SygusSolver::assertSygusInvConstraint(Node inv,
96
                                           Node pre,
97
                                           Node trans,
98
                                           Node post)
99
{
100
62
  Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
101
31
               << " " << trans << " " << post << "\n";
102
  // build invariant constraint
103
104
  // get variables (regular and their respective primed versions)
105
62
  std::vector<Node> terms;
106
62
  std::vector<Node> vars;
107
62
  std::vector<Node> primed_vars;
108
31
  terms.push_back(inv);
109
31
  terms.push_back(pre);
110
31
  terms.push_back(trans);
111
31
  terms.push_back(post);
112
  // variables are built based on the invariant type
113
31
  NodeManager* nm = NodeManager::currentNM();
114
62
  std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
115
220
  for (const TypeNode& tn : argTypes)
116
  {
117
189
    vars.push_back(nm->mkBoundVar(tn));
118
189
    d_sygusVars.push_back(vars.back());
119
378
    std::stringstream ss;
120
189
    ss << vars.back() << "'";
121
189
    primed_vars.push_back(nm->mkBoundVar(ss.str(), tn));
122
189
    d_sygusVars.push_back(primed_vars.back());
123
  }
124
125
  // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
126
155
  for (unsigned i = 0; i < 4; ++i)
127
  {
128
248
    Node op = terms[i];
129
248
    Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
130
124
                       << " with type " << op.getType() << "...\n";
131
248
    std::vector<Node> children;
132
124
    children.push_back(op);
133
    // transition relation applied over both variable lists
134
124
    if (i == 2)
135
    {
136
31
      children.insert(children.end(), vars.begin(), vars.end());
137
31
      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
138
    }
139
    else
140
    {
141
93
      children.insert(children.end(), vars.begin(), vars.end());
142
    }
143
124
    terms[i] = nm->mkNode(APPLY_UF, children);
144
    // make application of Inv on primed variables
145
124
    if (i == 0)
146
    {
147
31
      children.clear();
148
31
      children.push_back(op);
149
31
      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
150
31
      terms.push_back(nm->mkNode(APPLY_UF, children));
151
    }
152
  }
153
  // make constraints
154
62
  std::vector<Node> conj;
155
31
  conj.push_back(nm->mkNode(IMPLIES, terms[1], terms[0]));
156
62
  Node term0_and_2 = nm->mkNode(AND, terms[0], terms[2]);
157
31
  conj.push_back(nm->mkNode(IMPLIES, term0_and_2, terms[4]));
158
31
  conj.push_back(nm->mkNode(IMPLIES, terms[0], terms[3]));
159
62
  Node constraint = nm->mkNode(AND, conj);
160
161
31
  d_sygusConstraints.push_back(constraint);
162
163
  // sygus conjecture is now stale
164
31
  setSygusConjectureStale();
165
31
}
166
167
372
Result SygusSolver::checkSynth(Assertions& as)
168
{
169
372
  if (options::incrementalSolving())
170
  {
171
    // TODO (project #7)
172
    throw ModalException(
173
        "Cannot make check-synth commands when incremental solving is enabled");
174
  }
175
372
  Trace("smt") << "SygusSolver::checkSynth" << std::endl;
176
744
  std::vector<Node> query;
177
372
  if (d_sygusConjectureStale)
178
  {
179
372
    NodeManager* nm = NodeManager::currentNM();
180
    // build synthesis conjecture from asserted constraints and declared
181
    // variables/functions
182
744
    std::vector<Node> bodyv;
183
372
    Trace("smt") << "Sygus : Constructing sygus constraint...\n";
184
372
    size_t nconstraints = d_sygusConstraints.size();
185
    Node body = nconstraints == 0
186
                    ? nm->mkConst(true)
187
202
                    : (nconstraints == 1 ? d_sygusConstraints[0]
188
946
                                         : nm->mkNode(AND, d_sygusConstraints));
189
372
    body = body.notNode();
190
372
    Trace("smt") << "...constructed sygus constraint " << body << std::endl;
191
372
    if (!d_sygusVars.empty())
192
    {
193
512
      Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars);
194
256
      body = nm->mkNode(EXISTS, boundVars, body);
195
256
      Trace("smt") << "...constructed exists " << body << std::endl;
196
    }
197
372
    if (!d_sygusFunSymbols.empty())
198
    {
199
372
      body =
200
744
          quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body);
201
    }
202
372
    Trace("smt") << "...constructed forall " << body << std::endl;
203
204
372
    Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
205
372
    if (Dump.isOn("raw-benchmark"))
206
    {
207
      d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
208
    }
209
210
372
    d_sygusConjectureStale = false;
211
212
    // TODO (project #7): if incremental, we should push a context and assert
213
372
    query.push_back(body);
214
  }
215
216
372
  Result r = d_smtSolver.checkSatisfiability(as, query, false, false);
217
218
  // Check that synthesis solutions satisfy the conjecture
219
720
  if (options::checkSynthSol()
220
720
      && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
221
  {
222
166
    checkSynthSolution(as);
223
  }
224
720
  return r;
225
}
226
227
84
bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map)
228
{
229
84
  Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
230
168
  std::map<Node, std::map<Node, Node>> sol_mapn;
231
  // fail if the theory engine does not have synthesis solutions
232
84
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
233
84
  if (qe == nullptr || !qe->getSynthSolutions(sol_mapn))
234
  {
235
    return false;
236
  }
237
164
  for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn)
238
  {
239
193
    for (std::pair<const Node, Node>& s : cs.second)
240
    {
241
113
      sol_map[s.first] = s.second;
242
    }
243
  }
244
84
  return true;
245
}
246
247
4
void SygusSolver::printSynthSolution(std::ostream& out)
248
{
249
4
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
250
4
  if (qe == nullptr)
251
  {
252
    InternalError()
253
        << "SygusSolver::printSynthSolution(): Cannot print synth solution in "
254
           "the current logic, which does not include quantifiers";
255
  }
256
4
  qe->printSynthSolution(out);
257
4
}
258
259
166
void SygusSolver::checkSynthSolution(Assertions& as)
260
{
261
166
  NodeManager* nm = NodeManager::currentNM();
262
167
  Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution"
263
1
           << std::endl;
264
332
  std::map<Node, std::map<Node, Node>> sol_map;
265
  // Get solutions and build auxiliary vectors for substituting
266
166
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
267
166
  if (qe == nullptr || !qe->getSynthSolutions(sol_map))
268
  {
269
    InternalError()
270
        << "SygusSolver::checkSynthSolution(): No solution to check!";
271
    return;
272
  }
273
166
  if (sol_map.empty())
274
  {
275
    InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
276
    return;
277
  }
278
166
  Trace("check-synth-sol") << "Got solution map:\n";
279
  // the set of synthesis conjectures in our assertions
280
332
  std::unordered_set<Node, NodeHashFunction> conjs;
281
  // For each of the above conjectures, the functions-to-synthesis and their
282
  // solutions. This is used as a substitution below.
283
332
  std::map<Node, std::vector<Node>> fvarMap;
284
332
  std::map<Node, std::vector<Node>> fsolMap;
285
332
  for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map)
286
  {
287
166
    Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n";
288
166
    conjs.insert(cmap.first);
289
166
    std::vector<Node>& fvars = fvarMap[cmap.first];
290
166
    std::vector<Node>& fsols = fsolMap[cmap.first];
291
421
    for (const std::pair<const Node, Node>& pair : cmap.second)
292
    {
293
510
      Trace("check-synth-sol")
294
255
          << "  " << pair.first << " --> " << pair.second << "\n";
295
255
      fvars.push_back(pair.first);
296
255
      fsols.push_back(pair.second);
297
    }
298
  }
299
166
  Trace("check-synth-sol") << "Starting new SMT Engine\n";
300
301
166
  Trace("check-synth-sol") << "Retrieving assertions\n";
302
  // Build conjecture from original assertions
303
166
  context::CDList<Node>* alist = as.getAssertionList();
304
166
  if (alist == nullptr)
305
  {
306
    Trace("check-synth-sol") << "No assertions to check\n";
307
    return;
308
  }
309
  // auxiliary assertions
310
332
  std::vector<Node> auxAssertions;
311
  // expand definitions cache
312
332
  std::unordered_map<Node, Node, NodeHashFunction> cache;
313
346
  for (Node assertion : *alist)
314
  {
315
181
    Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
316
1
             << assertion << std::endl;
317
180
    Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
318
    // Apply any define-funs from the problem.
319
360
    Node n = d_pp.expandDefinitions(assertion, cache);
320
181
    Notice() << "SygusSolver::checkSynthSolution(): -- expands to " << n
321
1
             << std::endl;
322
180
    Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
323
180
    if (conjs.find(n) == conjs.end())
324
    {
325
173
      Trace("check-synth-sol") << "It is an auxiliary assertion\n";
326
173
      auxAssertions.push_back(n);
327
    }
328
    else
329
    {
330
7
      Trace("check-synth-sol") << "It is a synthesis conjecture\n";
331
    }
332
  }
333
  // check all conjectures
334
332
  for (Node conj : conjs)
335
  {
336
    // Start new SMT engine to check solutions
337
332
    std::unique_ptr<SmtEngine> solChecker;
338
166
    initializeSubsolver(solChecker);
339
166
    solChecker->getOptions().set(options::checkSynthSol, false);
340
250223
    solChecker->getOptions().set(options::sygusRecFun, false);
341
    // get the solution for this conjecture
342
166
    std::vector<Node>& fvars = fvarMap[conj];
343
166
    std::vector<Node>& fsols = fsolMap[conj];
344
    // Apply solution map to conjecture body
345
332
    Node conjBody;
346
    /* Whether property is quantifier free */
347
166
    if (conj[1].getKind() != EXISTS)
348
    {
349
166
      conjBody = conj[1].substitute(
350
          fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
351
    }
352
    else
353
    {
354
      conjBody = conj[1][1].substitute(
355
          fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
356
357
      /* Skolemize property */
358
      std::vector<Node> vars, skos;
359
      for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
360
      {
361
        vars.push_back(conj[1][0][j]);
362
        std::stringstream ss;
363
        ss << "sk_" << j;
364
        skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
365
        Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
366
                                 << skos.back() << "\n";
367
      }
368
      conjBody = conjBody.substitute(
369
          vars.begin(), vars.end(), skos.begin(), skos.end());
370
    }
371
167
    Notice() << "SygusSolver::checkSynthSolution(): -- body substitutes to "
372
1
             << conjBody << std::endl;
373
332
    Trace("check-synth-sol")
374
166
        << "Substituted body of assertion to " << conjBody << "\n";
375
166
    solChecker->assertFormula(conjBody);
376
    // Assert all auxiliary assertions. This may include recursive function
377
    // definitions that were added as assertions to the sygus problem.
378
339
    for (Node a : auxAssertions)
379
    {
380
173
      solChecker->assertFormula(a);
381
    }
382
332
    Result r = solChecker->checkSat();
383
167
    Notice() << "SygusSolver::checkSynthSolution(): result is " << r
384
1
             << std::endl;
385
166
    Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
386
166
    if (r.asSatisfiabilityResult().isUnknown())
387
    {
388
      InternalError() << "SygusSolver::checkSynthSolution(): could not check "
389
                         "solution, result "
390
                         "unknown.";
391
    }
392
166
    else if (r.asSatisfiabilityResult().isSat())
393
    {
394
      InternalError()
395
          << "SygusSolver::checkSynthSolution(): produced solution leads to "
396
             "satisfiable negated conjecture.";
397
    }
398
  }
399
}
400
401
1807
void SygusSolver::setSygusConjectureStale()
402
{
403
1807
  if (d_sygusConjectureStale)
404
  {
405
    // already stale
406
1807
    return;
407
  }
408
  d_sygusConjectureStale = true;
409
  // TODO (project #7): if incremental, we should pop a context
410
}
411
412
}  // namespace smt
413
276733
}  // namespace CVC4