1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
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 sygus_grammar_red. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/sygus_grammar_red.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "expr/sygus_datatype.h" |
21 |
|
#include "options/quantifiers_options.h" |
22 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
23 |
|
#include "theory/quantifiers/term_util.h" |
24 |
|
#include "theory/rewriter.h" |
25 |
|
|
26 |
|
using namespace std; |
27 |
|
using namespace cvc5::kind; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace quantifiers { |
32 |
|
|
33 |
446 |
void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn) |
34 |
|
{ |
35 |
446 |
Assert(tds != nullptr); |
36 |
446 |
Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl; |
37 |
446 |
d_type = tn; |
38 |
446 |
Assert(tn.isDatatype()); |
39 |
446 |
tds->registerSygusType(tn); |
40 |
446 |
const DType& dt = tn.getDType(); |
41 |
446 |
Assert(dt.isSygus()); |
42 |
892 |
TypeNode btn = dt.getSygusType(); |
43 |
2605 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
44 |
|
{ |
45 |
4318 |
Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?" |
46 |
2159 |
<< std::endl; |
47 |
4318 |
Node sop = dt[i].getSygusOp(); |
48 |
2159 |
if (sop.getAttribute(SygusAnyConstAttribute())) |
49 |
|
{ |
50 |
|
// the any constant constructor is never redundant |
51 |
|
d_sygus_red_status.push_back(0); |
52 |
|
continue; |
53 |
|
} |
54 |
4318 |
std::map<int, Node> pre; |
55 |
|
// We do not do beta reduction, since we want the arguments to match the |
56 |
|
// the types of the datatype. |
57 |
4318 |
Node g = tds->mkGeneric(dt, i, pre, false); |
58 |
2159 |
Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl; |
59 |
2159 |
d_gen_terms[i] = g; |
60 |
|
// is the operator a lambda of the form (lambda x1...xn. f(x1...xn))? |
61 |
2159 |
bool lamInOrder = false; |
62 |
2159 |
if (sop.getKind() == LAMBDA && sop[0].getNumChildren() == sop[1].getNumChildren()) |
63 |
|
{ |
64 |
951 |
Assert(g.getNumChildren()==sop[0].getNumChildren()); |
65 |
951 |
lamInOrder = true; |
66 |
2743 |
for (size_t j = 0, nchild = sop[1].getNumChildren(); j < nchild; j++) |
67 |
|
{ |
68 |
1798 |
if (sop[0][j] != sop[1][j]) |
69 |
|
{ |
70 |
|
// arguments not in order |
71 |
6 |
lamInOrder = false; |
72 |
6 |
break; |
73 |
|
} |
74 |
|
} |
75 |
|
} |
76 |
|
// a list of variants of the generic term (see getGenericList). |
77 |
4318 |
std::vector<Node> glist; |
78 |
2159 |
if (lamInOrder) |
79 |
|
{ |
80 |
|
// If it is a lambda whose arguments are one-to-one with the datatype |
81 |
|
// arguments, then we can add variants of this operator by permuting |
82 |
|
// the argument list (see getGenericList). |
83 |
945 |
Assert(g.getNumChildren()==dt[i].getNumArgs()); |
84 |
2734 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
85 |
|
{ |
86 |
1789 |
pre[j] = g[j]; |
87 |
|
} |
88 |
945 |
getGenericList(tds, dt, i, 0, pre, glist); |
89 |
|
} |
90 |
|
else |
91 |
|
{ |
92 |
|
// It is a builtin (possibly) ground term. Its children do not correspond |
93 |
|
// one-to-one with the arugments of the constructor. Hence, we consider |
94 |
|
// only g itself as a variant. |
95 |
1214 |
glist.push_back(g); |
96 |
|
} |
97 |
|
// call the extended rewriter |
98 |
2159 |
bool red = false; |
99 |
5017 |
for (const Node& gr : glist) |
100 |
|
{ |
101 |
2879 |
Trace("sygus-red-debug") << " ...variant : " << gr << std::endl; |
102 |
2879 |
std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr); |
103 |
2879 |
if (itg != d_gen_cons.end() && itg->second != i) |
104 |
|
{ |
105 |
21 |
red = true; |
106 |
42 |
Trace("sygus-red") << " ......redundant, since a variant of " << g |
107 |
21 |
<< " and " << d_gen_terms[itg->second] |
108 |
21 |
<< " both rewrite to " << gr << std::endl; |
109 |
21 |
break; |
110 |
|
} |
111 |
|
else |
112 |
|
{ |
113 |
2858 |
d_gen_cons[gr] = i; |
114 |
2858 |
Trace("sygus-red") << " ......not redundant." << std::endl; |
115 |
|
} |
116 |
|
} |
117 |
2159 |
d_sygus_red_status.push_back(red ? 1 : 0); |
118 |
|
} |
119 |
892 |
Trace("sygus-red") << "Compute redundant cons for " << tn << " finished" |
120 |
446 |
<< std::endl; |
121 |
446 |
} |
122 |
|
|
123 |
446 |
void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices) |
124 |
|
{ |
125 |
446 |
const DType& dt = d_type.getDType(); |
126 |
2605 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
127 |
|
{ |
128 |
2159 |
if (isRedundant(i)) |
129 |
|
{ |
130 |
21 |
indices.push_back(i); |
131 |
|
} |
132 |
|
} |
133 |
446 |
} |
134 |
|
|
135 |
2159 |
bool SygusRedundantCons::isRedundant(unsigned i) |
136 |
|
{ |
137 |
2159 |
Assert(i < d_sygus_red_status.size()); |
138 |
2159 |
return d_sygus_red_status[i] == 1; |
139 |
|
} |
140 |
|
|
141 |
4287 |
void SygusRedundantCons::getGenericList(TermDbSygus* tds, |
142 |
|
const DType& dt, |
143 |
|
unsigned c, |
144 |
|
unsigned index, |
145 |
|
std::map<int, Node>& pre, |
146 |
|
std::vector<Node>& terms) |
147 |
|
{ |
148 |
4287 |
if (index == dt[c].getNumArgs()) |
149 |
|
{ |
150 |
3368 |
Node gt = tds->mkGeneric(dt, c, pre); |
151 |
1684 |
gt = Rewriter::callExtendedRewrite(gt); |
152 |
1684 |
terms.push_back(gt); |
153 |
1684 |
return; |
154 |
|
} |
155 |
|
// with no swap |
156 |
2603 |
getGenericList(tds, dt, c, index + 1, pre, terms); |
157 |
|
// swapping is exponential, only use for operators with small # args. |
158 |
2603 |
if (dt[c].getNumArgs() <= 5) |
159 |
|
{ |
160 |
5206 |
TypeNode atype = tds->getArgType(dt[c], index); |
161 |
3654 |
for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++) |
162 |
|
{ |
163 |
1051 |
if (tds->getArgType(dt[c], s) == atype) |
164 |
|
{ |
165 |
|
// swap s and index |
166 |
1478 |
Node tmp = pre[s]; |
167 |
739 |
pre[s] = pre[index]; |
168 |
739 |
pre[index] = tmp; |
169 |
739 |
getGenericList(tds, dt, c, index + 1, pre, terms); |
170 |
|
// revert |
171 |
739 |
tmp = pre[s]; |
172 |
739 |
pre[s] = pre[index]; |
173 |
739 |
pre[index] = tmp; |
174 |
|
} |
175 |
|
} |
176 |
|
} |
177 |
|
} |
178 |
|
|
179 |
|
} // namespace quantifiers |
180 |
|
} // namespace theory |
181 |
29577 |
} // namespace cvc5 |