GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_interpol.cpp Lines: 151 179 84.4 %
Date: 2021-03-22 Branches: 271 680 39.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_interpol.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Ying Sheng, Abdalrhman Mohamed, Andrew Reynolds
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 interpolation utility, which
13
 ** transforms an input of axioms and conjecture into an interpolation problem,
14
 *and solve it.
15
 **/
16
17
#include "theory/quantifiers/sygus/sygus_interpol.h"
18
19
#include <sstream>
20
21
#include "expr/dtype.h"
22
#include "expr/node_algorithm.h"
23
#include "options/smt_options.h"
24
#include "theory/datatypes/sygus_datatype_utils.h"
25
#include "theory/quantifiers/quantifiers_attributes.h"
26
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
27
#include "theory/rewriter.h"
28
#include "theory/smt_engine_subsolver.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace quantifiers {
33
34
10
SygusInterpol::SygusInterpol() {}
35
36
10
void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
37
                                   const Node& conj)
38
{
39
10
  Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
40
20
  std::unordered_set<Node, NodeHashFunction> symSetAxioms;
41
20
  std::unordered_set<Node, NodeHashFunction> symSetConj;
42
25
  for (size_t i = 0, size = axioms.size(); i < size; i++)
43
  {
44
15
    expr::getSymbols(axioms[i], symSetAxioms);
45
  }
46
10
  expr::getSymbols(conj, symSetConj);
47
10
  d_syms.insert(d_syms.end(), symSetAxioms.begin(), symSetAxioms.end());
48
10
  d_syms.insert(d_syms.end(), symSetConj.begin(), symSetConj.end());
49
36
  for (const Node& elem : symSetConj)
50
  {
51
26
    if (symSetAxioms.find(elem) != symSetAxioms.end())
52
    {
53
16
      d_symSetShared.insert(elem);
54
    }
55
  }
56
20
  Trace("sygus-interpol-debug")
57
20
      << "...finish, got " << d_syms.size() << " symbols in total. And "
58
10
      << d_symSetShared.size() << " shared symbols." << std::endl;
59
10
}
60
61
10
void SygusInterpol::createVariables(bool needsShared)
62
{
63
10
  NodeManager* nm = NodeManager::currentNM();
64
113
  for (const Node& s : d_syms)
65
  {
66
206
    TypeNode tn = s.getType();
67
103
    if (tn.isConstructor() || tn.isSelector() || tn.isTester())
68
    {
69
      // datatype symbols should be considered interpreted symbols here, not
70
      // (higher-order) variables.
71
      continue;
72
    }
73
    // Notice that we allow for non-first class (e.g. function) variables here.
74
206
    std::stringstream ss;
75
103
    ss << s;
76
206
    Node var = nm->mkBoundVar(tn);
77
103
    d_vars.push_back(var);
78
206
    Node vlv = nm->mkBoundVar(ss.str(), tn);
79
    // set that this variable encodes the term s
80
    SygusVarToTermAttribute sta;
81
103
    vlv.setAttribute(sta, s);
82
103
    d_vlvs.push_back(vlv);
83
103
    if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
84
    {
85
34
      d_varsShared.push_back(var);
86
34
      d_vlvsShared.push_back(vlv);
87
34
      d_varTypesShared.push_back(tn);
88
    }
89
  }
90
  // make the sygus variable list
91
10
  d_ibvlShared = nm->mkNode(kind::BOUND_VAR_LIST, d_vlvsShared);
92
10
  Trace("sygus-interpol-debug") << "...finish" << std::endl;
93
10
}
94
95
9
void SygusInterpol::getIncludeCons(
96
    const std::vector<Node>& axioms,
97
    const Node& conj,
98
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result)
99
{
100
9
  NodeManager* nm = NodeManager::currentNM();
101
9
  Assert(options::produceInterpols() != options::ProduceInterpols::NONE);
102
  // ASSUMPTIONS
103
9
  if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS)
104
  {
105
    Node tmpAssumptions =
106
        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
107
    expr::getOperatorsMap(tmpAssumptions, result);
108
  }
109
  // CONJECTURE
110
9
  else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE)
111
  {
112
1
    expr::getOperatorsMap(conj, result);
113
  }
114
  // SHARED
115
8
  else if (options::produceInterpols() == options::ProduceInterpols::SHARED)
116
  {
117
    // Get operators from axioms
118
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
119
        include_cons_axioms;
120
    Node tmpAssumptions =
121
        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
122
    expr::getOperatorsMap(tmpAssumptions, include_cons_axioms);
123
124
    // Get operators from conj
125
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
126
        include_cons_conj;
127
    expr::getOperatorsMap(conj, include_cons_conj);
128
129
    // Compute intersection
130
    for (std::map<TypeNode,
131
                  std::unordered_set<Node, NodeHashFunction>>::iterator it =
132
             include_cons_axioms.begin();
133
         it != include_cons_axioms.end();
134
         it++)
135
    {
136
      TypeNode tn = it->first;
137
      std::unordered_set<Node, NodeHashFunction> axiomsOps = it->second;
138
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
139
          concIter = include_cons_conj.find(tn);
140
      if (concIter != include_cons_conj.end())
141
      {
142
        std::unordered_set<Node, NodeHashFunction> conjOps = concIter->second;
143
        for (const Node& n : axiomsOps)
144
        {
145
          if (conjOps.find(n) != conjOps.end())
146
          {
147
            if (result.find(tn) == result.end())
148
            {
149
              result[tn] = std::unordered_set<Node, NodeHashFunction>();
150
            }
151
            result[tn].insert(n);
152
          }
153
        }
154
      }
155
    }
156
  }
157
  // ALL
158
8
  else if (options::produceInterpols() == options::ProduceInterpols::ALL)
159
  {
160
    Node tmpAssumptions =
161
        (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
162
    Node tmpAll = nm->mkNode(kind::AND, tmpAssumptions, conj);
163
    expr::getOperatorsMap(tmpAll, result);
164
  }
165
9
}
166
167
10
TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
168
                                        const std::vector<Node>& axioms,
169
                                        const Node& conj)
170
{
171
10
  Trace("sygus-interpol-debug") << "Setup grammar..." << std::endl;
172
10
  TypeNode itpGTypeS;
173
10
  if (!itpGType.isNull())
174
  {
175
    // set user-defined grammar
176
1
    Assert(itpGType.isDatatype() && itpGType.getDType().isSygus());
177
1
    itpGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
178
        itpGType, d_syms, d_vlvs);
179
1
    Assert(itpGTypeS.isDatatype() && itpGTypeS.getDType().isSygus());
180
    // TODO(Ying Sheng) check if the vars in user-defined grammar, are
181
    // consistent with the shared vars
182
  }
183
  else
184
  {
185
    // set default grammar
186
18
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
187
18
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
188
18
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
189
9
    getIncludeCons(axioms, conj, include_cons);
190
18
    std::unordered_set<Node, NodeHashFunction> terms_irrelevant;
191
27
    itpGTypeS = CegGrammarConstructor::mkSygusDefaultType(
192
18
        NodeManager::currentNM()->booleanType(),
193
        d_ibvlShared,
194
        "interpolation_grammar",
195
        extra_cons,
196
        exclude_cons,
197
        include_cons,
198
        terms_irrelevant);
199
  }
200
10
  Trace("sygus-interpol-debug") << "...finish setting up grammar" << std::endl;
201
10
  return itpGTypeS;
202
}
203
204
10
Node SygusInterpol::mkPredicate(const std::string& name)
205
{
206
10
  NodeManager* nm = NodeManager::currentNM();
207
  // make the interpolation predicate to synthesize
208
20
  Trace("sygus-interpol-debug")
209
10
      << "Make interpolation predicate..." << std::endl;
210
10
  TypeNode itpType = d_varTypesShared.empty()
211
                         ? nm->booleanType()
212
20
                         : nm->mkPredicateType(d_varTypesShared);
213
10
  Node itp = nm->mkBoundVar(name.c_str(), itpType);
214
10
  Trace("sygus-interpol-debug") << "...finish" << std::endl;
215
20
  return itp;
216
}
217
218
10
void SygusInterpol::mkSygusConjecture(Node itp,
219
                                      const std::vector<Node>& axioms,
220
                                      const Node& conj)
221
{
222
10
  NodeManager* nm = NodeManager::currentNM();
223
  // make the interpolation application to synthesize
224
20
  Trace("sygus-interpol-debug")
225
10
      << "Make interpolation predicate app..." << std::endl;
226
20
  std::vector<Node> ichildren;
227
10
  ichildren.push_back(itp);
228
10
  ichildren.insert(ichildren.end(), d_varsShared.begin(), d_varsShared.end());
229
  Node itpApp =
230
20
      d_varsShared.empty() ? itp : nm->mkNode(kind::APPLY_UF, ichildren);
231
20
  Trace("sygus-interpol-debug") << "itpApp: " << itpApp << std::endl
232
10
                                << std::endl;
233
10
  Trace("sygus-interpol-debug") << "...finish" << std::endl;
234
235
  // set the sygus bound variable list
236
10
  Trace("sygus-interpol-debug") << "Set attributes..." << std::endl;
237
10
  itp.setAttribute(SygusSynthFunVarListAttribute(), d_ibvlShared);
238
10
  Trace("sygus-interpol-debug") << "...finish" << std::endl;
239
240
  // Fa( x )
241
10
  Trace("sygus-interpol-debug") << "Make conjecture body..." << std::endl;
242
20
  Node Fa = axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms);
243
  // Fa( x ) => A( x )
244
20
  Node firstImplication = nm->mkNode(kind::IMPLIES, Fa, itpApp);
245
20
  Trace("sygus-interpol-debug")
246
10
      << "first implication: " << firstImplication << std::endl
247
10
      << std::endl;
248
  // A( x ) => Fc( x )
249
20
  Node Fc = conj;
250
20
  Node secondImplication = nm->mkNode(kind::IMPLIES, itpApp, Fc);
251
20
  Trace("sygus-interpol-debug")
252
10
      << "second implication: " << secondImplication << std::endl
253
10
      << std::endl;
254
  // Fa( x ) => A( x ) ^ A( x ) => Fc( x )
255
20
  Node constraint = nm->mkNode(kind::AND, firstImplication, secondImplication);
256
10
  constraint = constraint.substitute(
257
      d_syms.begin(), d_syms.end(), d_vars.begin(), d_vars.end());
258
10
  Trace("sygus-interpol-debug") << constraint << "...finish" << std::endl;
259
10
  constraint = Rewriter::rewrite(constraint);
260
261
10
  d_sygusConj = constraint;
262
10
  Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
263
10
}
264
265
10
bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp)
266
{
267
  // get the synthesis solution
268
20
  std::map<Node, Node> sols;
269
10
  subSolver->getSynthSolutions(sols);
270
10
  Assert(sols.size() == 1);
271
10
  std::map<Node, Node>::iterator its = sols.find(itp);
272
10
  if (its == sols.end())
273
  {
274
    Trace("sygus-interpol")
275
        << "SmtEngine::getInterpol: could not find solution!" << std::endl;
276
    throw RecoverableModalException(
277
        "Could not find solution for get-interpol.");
278
    return false;
279
  }
280
20
  Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
281
10
                          << its->second << std::endl;
282
10
  interpol = its->second;
283
  // replace back the created variables to original symbols.
284
10
  if (interpol.getKind() == kind::LAMBDA)
285
  {
286
10
    interpol = interpol[1];
287
  }
288
289
  // get the grammar type for the interpolant
290
20
  Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute());
291
10
  Assert(!igdtbv.isNull());
292
10
  Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST);
293
  // convert back to original
294
  // must replace formal arguments of itp with the free variables in the
295
  // input problem that they correspond to.
296
20
  std::vector<Node> vars;
297
20
  std::vector<Node> syms;
298
  SygusVarToTermAttribute sta;
299
44
  for (const Node& bv : igdtbv)
300
  {
301
34
    vars.push_back(bv);
302
34
    syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
303
  }
304
10
  interpol =
305
20
      interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
306
307
10
  return true;
308
}
309
310
10
bool SygusInterpol::solveInterpolation(const std::string& name,
311
                                       const std::vector<Node>& axioms,
312
                                       const Node& conj,
313
                                       const TypeNode& itpGType,
314
                                       Node& interpol)
315
{
316
  // Some instructions in setSynthGrammar and mkSygusConjecture need a fully
317
  // initialized solver to work properly. Notice, however, that the sub-solver
318
  // created below is not fully initialized by the time those two methods are
319
  // needed. Therefore, we call them while the current parent solver is in scope
320
  // (i.e., before creating the sub-solver).
321
10
  collectSymbols(axioms, conj);
322
10
  createVariables(itpGType.isNull());
323
20
  TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj);
324
325
20
  Node itp = mkPredicate(name);
326
10
  mkSygusConjecture(itp, axioms, conj);
327
328
20
  std::unique_ptr<SmtEngine> subSolver;
329
10
  initializeSubsolver(subSolver);
330
  // get the logic
331
20
  LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
332
  // enable everything needed for sygus
333
10
  l.enableSygus();
334
10
  subSolver->setLogic(l);
335
336
113
  for (const Node& var : d_vars)
337
  {
338
103
    subSolver->declareSygusVar(var);
339
  }
340
20
  std::vector<Node> vars_empty;
341
10
  subSolver->declareSynthFun(itp, grammarType, false, vars_empty);
342
20
  Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : "
343
10
                          << d_sygusConj << ", solving for "
344
10
                          << d_sygusConj[0][0] << std::endl;
345
10
  subSolver->assertSygusConstraint(d_sygusConj);
346
347
20
  Trace("sygus-interpol") << "  SmtEngine::getInterpol check sat..."
348
10
                          << std::endl;
349
20
  Result r = subSolver->checkSynth();
350
20
  Trace("sygus-interpol") << "  SmtEngine::getInterpol result: " << r
351
10
                          << std::endl;
352
10
  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
353
  {
354
10
    return findInterpol(subSolver.get(), interpol, itp);
355
  }
356
  return false;
357
}
358
359
}  // namespace quantifiers
360
}  // namespace theory
361
26676
}  // namespace CVC4