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