GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_abduct.cpp Lines: 82 83 98.8 %
Date: 2021-03-22 Branches: 208 446 46.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_abduct.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 Implementation of sygus abduction utility, which
13
 ** transforms an arbitrary input into an abduction problem.
14
 **/
15
16
#include "theory/quantifiers/sygus/sygus_abduct.h"
17
18
#include <sstream>
19
20
#include "expr/dtype.h"
21
#include "expr/node_algorithm.h"
22
#include "expr/sygus_datatype.h"
23
#include "theory/datatypes/sygus_datatype_utils.h"
24
#include "theory/quantifiers/quantifiers_attributes.h"
25
#include "theory/quantifiers/quantifiers_rewriter.h"
26
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
27
#include "theory/quantifiers/sygus/sygus_utils.h"
28
#include "theory/quantifiers/term_util.h"
29
#include "theory/rewriter.h"
30
31
using namespace std;
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace quantifiers {
37
38
SygusAbduct::SygusAbduct() {}
39
40
22
Node SygusAbduct::mkAbductionConjecture(const std::string& name,
41
                                        const std::vector<Node>& asserts,
42
                                        const std::vector<Node>& axioms,
43
                                        TypeNode abdGType)
44
{
45
22
  NodeManager* nm = NodeManager::currentNM();
46
44
  std::unordered_set<Node, NodeHashFunction> symset;
47
184
  for (size_t i = 0, size = asserts.size(); i < size; i++)
48
  {
49
162
    expr::getSymbols(asserts[i], symset);
50
  }
51
44
  Trace("sygus-abduct-debug")
52
22
      << "...finish, got " << symset.size() << " symbols." << std::endl;
53
54
22
  Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
55
44
  std::vector<Node> syms;
56
44
  std::vector<Node> vars;
57
44
  std::vector<Node> varlist;
58
44
  std::vector<TypeNode> varlistTypes;
59
160
  for (const Node& s : symset)
60
  {
61
268
    TypeNode tn = s.getType();
62
138
    if (tn.isConstructor() || tn.isSelector() || tn.isTester())
63
    {
64
      // datatype symbols should be considered interpreted symbols here, not
65
      // (higher-order) variables.
66
8
      continue;
67
    }
68
    // Notice that we allow for non-first class (e.g. function) variables here.
69
    // This is applicable to the case where we are doing get-abduct in a logic
70
    // with UF.
71
260
    std::stringstream ss;
72
130
    ss << s;
73
260
    Node var = nm->mkBoundVar(tn);
74
130
    syms.push_back(s);
75
130
    vars.push_back(var);
76
260
    Node vlv = nm->mkBoundVar(ss.str(), tn);
77
130
    varlist.push_back(vlv);
78
130
    varlistTypes.push_back(tn);
79
    // set that this variable encodes the term s
80
    SygusVarToTermAttribute sta;
81
130
    vlv.setAttribute(sta, s);
82
  }
83
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
84
85
22
  Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl;
86
  // make the abduction predicate to synthesize
87
22
  TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
88
44
                                          : nm->mkPredicateType(varlistTypes);
89
44
  Node abd = nm->mkBoundVar(name.c_str(), abdType);
90
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
91
92
  // the sygus variable list
93
44
  Node abvl;
94
  // if provided, we will associate the provide sygus datatype type with the
95
  // function-to-synthesize. However, we must convert it so that its
96
  // free symbols are universally quantified.
97
22
  if (!abdGType.isNull())
98
  {
99
8
    Assert(abdGType.isDatatype() && abdGType.getDType().isSygus());
100
8
    Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
101
8
    Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl;
102
103
    // substitute the free symbols of the grammar with variables corresponding
104
    // to the formal argument list of the new sygus datatype type.
105
    TypeNode abdGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
106
16
        abdGType, syms, varlist);
107
108
8
    Assert(abdGTypeS.isDatatype() && abdGTypeS.getDType().isSygus());
109
110
16
    Trace("sygus-abduct-debug")
111
8
        << "Make sygus grammar attribute..." << std::endl;
112
16
    Node sym = nm->mkBoundVar("sfproxy_abduct", abdGTypeS);
113
    // Set the sygus grammar attribute to indicate that abdGTypeS encodes the
114
    // grammar for abd.
115
    theory::SygusSynthGrammarAttribute ssg;
116
8
    abd.setAttribute(ssg, sym);
117
8
    Trace("sygus-abduct-debug") << "Finished setting up grammar." << std::endl;
118
119
    // use the bound variable list from the new substituted grammar type
120
8
    const DType& agtsd = abdGTypeS.getDType();
121
8
    abvl = agtsd.getSygusVarList();
122
8
    Assert(!abvl.isNull() && abvl.getKind() == BOUND_VAR_LIST);
123
  }
124
  else
125
  {
126
    // the bound variable list of the abduct-to-synthesize is determined by
127
    // the variable list above
128
14
    abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
129
    // We do not set a grammar type for abd (SygusSynthGrammarAttribute).
130
    // Its grammar will be constructed internally in the default way
131
  }
132
133
22
  Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl;
134
44
  std::vector<Node> achildren;
135
22
  achildren.push_back(abd);
136
22
  achildren.insert(achildren.end(), vars.begin(), vars.end());
137
44
  Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren);
138
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
139
140
22
  Trace("sygus-abduct-debug") << "Set attributes..." << std::endl;
141
  // set the sygus bound variable list
142
22
  abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl);
143
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
144
145
22
  Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl;
146
44
  Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts);
147
22
  input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
148
  // A(x) => ~input( x )
149
22
  input = nm->mkNode(OR, abdApp.negate(), input.negate());
150
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
151
152
22
  Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl;
153
22
  Node res = input.negate();
154
22
  if (!vars.empty())
155
  {
156
44
    Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
157
    // exists x. ~( A( x ) => ~input( x ) )
158
22
    res = nm->mkNode(EXISTS, bvl, res);
159
  }
160
  // sygus attribute
161
22
  Node aconj = axioms.size() == 0
162
                   ? nm->mkConst(true)
163
44
                   : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms));
164
22
  aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
165
22
  Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
166
44
  Node sc = nm->mkNode(AND, aconj, abdApp);
167
44
  Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
168
22
  sc = nm->mkNode(EXISTS, vbvl, sc);
169
44
  Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
170
22
  sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
171
44
  Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
172
  // build in the side condition
173
  //   exists x. A( x ) ^ input_axioms( x )
174
  // as an additional annotation on the sygus conjecture. In other words,
175
  // the abducts A we procedure must be consistent with our axioms.
176
177
  // forall A. exists x. ~( A( x ) => ~input( x ) )
178
22
  res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr});
179
22
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
180
181
22
  res = theory::Rewriter::rewrite(res);
182
183
22
  Trace("sygus-abduct") << "Generate: " << res << std::endl;
184
185
44
  return res;
186
}
187
188
}  // namespace quantifiers
189
}  // namespace theory
190
26676
}  // namespace CVC4