GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_utils.cpp Lines: 57 76 75.0 %
Date: 2021-03-22 Branches: 110 366 30.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 generic sygus utilities
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_utils.h"
16
17
#include <sstream>
18
19
#include "expr/node_algorithm.h"
20
#include "theory/quantifiers/quantifiers_attributes.h"
21
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
/**
30
 * Attribute for specifying a solution for a function-to-synthesize. This is
31
 * used for marking certain functions that we have solved for, e.g. during
32
 * preprocessing.
33
 */
34
struct SygusSolutionAttributeId
35
{
36
};
37
typedef expr::Attribute<SygusSolutionAttributeId, Node> SygusSolutionAttribute;
38
39
448
Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
40
                                   Node conj,
41
                                   const std::vector<Node>& iattrs)
42
{
43
448
  Assert(!fs.empty());
44
448
  NodeManager* nm = NodeManager::currentNM();
45
  SygusAttribute ca;
46
896
  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
47
448
  sygusVar.setAttribute(ca, true);
48
896
  std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
49
  // insert the remaining instantiation attributes
50
448
  ipls.insert(ipls.end(), iattrs.begin(), iattrs.end());
51
896
  Node ipl = nm->mkNode(INST_PATTERN_LIST, ipls);
52
896
  Node bvl = nm->mkNode(BOUND_VAR_LIST, fs);
53
896
  return nm->mkNode(FORALL, bvl, conj, ipl);
54
}
55
56
426
Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs, Node conj)
57
{
58
852
  std::vector<Node> iattrs;
59
852
  return mkSygusConjecture(fs, conj, iattrs);
60
}
61
62
Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
63
                                   Node conj,
64
                                   const Subs& solvedf)
65
{
66
  Assert(!fs.empty());
67
  NodeManager* nm = NodeManager::currentNM();
68
  std::vector<Node> iattrs;
69
  // take existing properties, without the previous solves
70
  SygusSolutionAttribute ssa;
71
  // add the current solves, which should be a superset of the previous ones
72
  for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
73
  {
74
    Node eq = solvedf.getEquality(i);
75
    Node var = nm->mkSkolem("solved", nm->booleanType());
76
    var.setAttribute(ssa, eq);
77
    Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
78
    iattrs.push_back(ipv);
79
  }
80
  return mkSygusConjecture(fs, conj, iattrs);
81
}
82
83
506
void SygusUtils::decomposeSygusConjecture(Node q,
84
                                          std::vector<Node>& fs,
85
                                          std::vector<Node>& unsf,
86
                                          Subs& solvedf)
87
{
88
506
  Assert(q.getKind() == FORALL);
89
506
  Assert(q.getNumChildren() == 3);
90
1012
  Node ipl = q[2];
91
506
  Assert(ipl.getKind() == INST_PATTERN_LIST);
92
506
  fs.insert(fs.end(), q[0].begin(), q[0].end());
93
  SygusSolutionAttribute ssa;
94
1034
  for (const Node& ip : ipl)
95
  {
96
528
    if (ip.getKind() == INST_ATTRIBUTE)
97
    {
98
1056
      Node ipv = ip[0];
99
      // does it specify a sygus solution?
100
528
      if (ipv.hasAttribute(ssa))
101
      {
102
        Node eq = ipv.getAttribute(ssa);
103
        Assert(std::find(fs.begin(), fs.end(), eq[0]) != fs.end());
104
        solvedf.addEquality(eq);
105
      }
106
    }
107
  }
108
  // add to unsolved functions
109
1289
  for (const Node& f : fs)
110
  {
111
783
    if (!solvedf.contains(f))
112
    {
113
783
      unsf.push_back(f);
114
    }
115
  }
116
506
}
117
118
Node SygusUtils::decomposeSygusBody(Node conj, std::vector<Node>& vs)
119
{
120
  if (conj.getKind() == NOT && conj[0].getKind() == FORALL)
121
  {
122
    vs.insert(vs.end(), conj[0][0].begin(), conj[0][0].end());
123
    return conj[0][1].negate();
124
  }
125
  return conj;
126
}
127
128
2310
Node SygusUtils::getSygusArgumentListForSynthFun(Node f)
129
{
130
2310
  Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
131
2310
  if (sfvl.isNull() && f.getType().isFunction())
132
  {
133
23
    NodeManager* nm = NodeManager::currentNM();
134
46
    std::vector<TypeNode> argTypes = f.getType().getArgTypes();
135
    // make default variable list if none was specified by input
136
46
    std::vector<Node> bvs;
137
49
    for (unsigned j = 0, size = argTypes.size(); j < size; j++)
138
    {
139
52
      std::stringstream ss;
140
26
      ss << "arg" << j;
141
26
      bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
142
    }
143
23
    sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
144
23
    f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
145
  }
146
2310
  return sfvl;
147
}
148
149
783
void SygusUtils::getSygusArgumentListForSynthFun(Node f,
150
                                                 std::vector<Node>& formals)
151
{
152
1566
  Node sfvl = getSygusArgumentListForSynthFun(f);
153
783
  if (!sfvl.isNull())
154
  {
155
612
    formals.insert(formals.end(), sfvl.begin(), sfvl.end());
156
  }
157
783
}
158
159
243
Node SygusUtils::wrapSolutionForSynthFun(Node f, Node sol)
160
{
161
486
  Node al = getSygusArgumentListForSynthFun(f);
162
243
  if (!al.isNull())
163
  {
164
198
    sol = NodeManager::currentNM()->mkNode(LAMBDA, al, sol);
165
  }
166
243
  Assert(!expr::hasFreeVar(sol));
167
486
  return sol;
168
}
169
170
115
TypeNode SygusUtils::getSygusTypeForSynthFun(Node f)
171
{
172
230
  Node gv = f.getAttribute(SygusSynthGrammarAttribute());
173
115
  if (!gv.isNull())
174
  {
175
58
    return gv.getType();
176
  }
177
57
  return TypeNode::null();
178
}
179
180
}  // namespace quantifiers
181
}  // namespace theory
182
26676
}  // namespace CVC4