1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of LFSC node conversion for list variables in side conditions |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/lfsc/lfsc_list_sc_node_converter.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace proof { |
20 |
|
|
21 |
|
LfscListScNodeConverter::LfscListScNodeConverter( |
22 |
|
LfscNodeConverter& conv, |
23 |
|
const std::unordered_set<Node>& listVars, |
24 |
|
bool isPre) |
25 |
|
: d_conv(conv), d_listVars(listVars), d_isPre(isPre) |
26 |
|
{ |
27 |
|
} |
28 |
|
|
29 |
|
Node LfscListScNodeConverter::postConvert(Node n) |
30 |
|
{ |
31 |
|
NodeManager* nm = NodeManager::currentNM(); |
32 |
|
Kind k = n.getKind(); |
33 |
|
if (d_isPre) |
34 |
|
{ |
35 |
|
// is this an application that may require nary elimination? |
36 |
|
if (NodeManager::isNAryKind(k)) |
37 |
|
{ |
38 |
|
size_t minLength = 0; |
39 |
|
for (const Node& nc : n) |
40 |
|
{ |
41 |
|
if (d_listVars.find(nc) == d_listVars.end()) |
42 |
|
{ |
43 |
|
minLength++; |
44 |
|
if (minLength >= 2) |
45 |
|
{ |
46 |
|
// no need to convert |
47 |
|
return n; |
48 |
|
} |
49 |
|
} |
50 |
|
} |
51 |
|
TypeNode tn = n.getType(); |
52 |
|
// if so, (or a b c) becomes (nary_elim f_or (or a b c) false), |
53 |
|
// where the children of this are converted |
54 |
|
std::vector<Node> children; |
55 |
|
Node f = d_conv.getOperatorOfTerm(n); |
56 |
|
children.push_back(f); |
57 |
|
// convert n, since this node will not be converted further |
58 |
|
children.push_back(d_conv.convert(n)); |
59 |
|
Node null = d_conv.getNullTerminator(k, tn); |
60 |
|
Assert(!null.isNull()); |
61 |
|
// likewise, convert null |
62 |
|
children.push_back(d_conv.convert(null)); |
63 |
|
Node sop = mkOperatorFor("nary_elim", children, tn); |
64 |
|
children.insert(children.begin(), sop); |
65 |
|
return nm->mkNode(kind::APPLY_UF, children); |
66 |
|
} |
67 |
|
return n; |
68 |
|
} |
69 |
|
Assert(k == kind::APPLY_UF || k == kind::APPLY_CONSTRUCTOR |
70 |
|
|| !NodeManager::isNAryKind(k) || n.getNumChildren() == 2) |
71 |
|
<< "Cannot convert LFSC side condition for " << n; |
72 |
|
// note that after converting to binary form, variables should only appear |
73 |
|
// as the first child of binary applications of n-ary operators |
74 |
|
if (n.getNumChildren() == 2 && d_listVars.find(n[0]) != d_listVars.end()) |
75 |
|
{ |
76 |
|
// this will fail if e.g. a list variable is a child of a non-n-ary kind |
77 |
|
Assert(NodeManager::isNAryKind(k)); |
78 |
|
TypeNode tn = n.getType(); |
79 |
|
// We are in converted form, but need to get the null terminator for the |
80 |
|
// original term. Hence, we convert the application back to original form |
81 |
|
// if we replaced with an APPLY_UF. |
82 |
|
if (k == kind::APPLY_UF) |
83 |
|
{ |
84 |
|
k = d_conv.getBuiltinKindForInternalSymbol(n.getOperator()); |
85 |
|
Assert(k != kind::UNDEFINED_KIND); |
86 |
|
// for uniformity, reconstruct in original form |
87 |
|
std::vector<Node> nchildren(n.begin(), n.end()); |
88 |
|
n = nm->mkNode(k, nchildren); |
89 |
|
} |
90 |
|
Node null = d_conv.getNullTerminator(k, tn); |
91 |
|
AlwaysAssert(!null.isNull()) |
92 |
|
<< "No null terminator for " << k << ", " << tn; |
93 |
|
null = d_conv.convert(null); |
94 |
|
// if a list variable occurs as a rightmost child, then we return just |
95 |
|
// the variable |
96 |
|
if (n[1] == null) |
97 |
|
{ |
98 |
|
return n[0]; |
99 |
|
} |
100 |
|
// E.g. (or x t) becomes (nary_concat f_or x t false) |
101 |
|
std::vector<Node> children; |
102 |
|
Node f = d_conv.getOperatorOfTerm(n); |
103 |
|
children.push_back(f); |
104 |
|
children.insert(children.end(), n.begin(), n.end()); |
105 |
|
children.push_back(null); |
106 |
|
Node sop = mkOperatorFor("nary_concat", children, tn); |
107 |
|
children.insert(children.begin(), sop); |
108 |
|
return nm->mkNode(kind::APPLY_UF, children); |
109 |
|
} |
110 |
|
return n; |
111 |
|
} |
112 |
|
|
113 |
|
Node LfscListScNodeConverter::mkOperatorFor(const std::string& name, |
114 |
|
const std::vector<Node>& children, |
115 |
|
TypeNode retType) |
116 |
|
{ |
117 |
|
NodeManager* nm = NodeManager::currentNM(); |
118 |
|
std::vector<TypeNode> childTypes; |
119 |
|
for (const Node& c : children) |
120 |
|
{ |
121 |
|
childTypes.push_back(c.getType()); |
122 |
|
} |
123 |
|
TypeNode ftype = nm->mkFunctionType(childTypes, retType); |
124 |
|
return d_conv.mkInternalSymbol(name, ftype); |
125 |
|
} |
126 |
|
|
127 |
|
} // namespace proof |
128 |
22746 |
} // namespace cvc5 |