73311b0bd50da4339d03d35cd9332cbaedb52c85
1 /********************* */
2 /*! \file sygus_grammar_norm.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief implementation of class for for simplifying SyGuS grammars after they
13 ** are encoded into datatypes.
16 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
18 #include "expr/datatype.h"
19 #include "options/quantifiers_options.h"
20 #include "printer/sygus_print_callback.h"
21 #include "smt/smt_engine.h"
22 #include "smt/smt_engine_scope.h"
23 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
24 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
25 #include "theory/quantifiers/sygus/term_database_sygus.h"
26 #include "theory/quantifiers/term_util.h"
28 #include <numeric> // for std::iota
30 using namespace CVC4::kind
;
34 namespace quantifiers
{
36 bool OpPosTrie::getOrMakeType(TypeNode tn
,
38 const std::vector
<unsigned>& op_pos
,
41 if (ind
== op_pos
.size())
44 if (!d_unres_tn
.isNull())
46 Trace("sygus-grammar-normalize-trie")
47 << "\tFound type " << d_unres_tn
<< "\n";
48 unres_tn
= d_unres_tn
;
51 /* Creating unresolved type */
54 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
56 ss
<< "_" << std::to_string(op_pos
[i
]);
58 d_unres_tn
= NodeManager::currentNM()->mkSort(
59 ss
.str(), ExprManager::SORT_FLAG_PLACEHOLDER
);
60 Trace("sygus-grammar-normalize-trie")
61 << "\tCreating type " << d_unres_tn
<< "\n";
62 unres_tn
= d_unres_tn
;
66 return d_children
[op_pos
[ind
]].getOrMakeType(tn
, unres_tn
, op_pos
, ind
+ 1);
69 void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm
* sygus_norm
,
70 const DatatypeConstructor
& cons
)
72 Trace("sygus-grammar-normalize") << "...for " << cons
.getName() << "\n";
73 /* Recover the sygus operator to not lose reference to the original
74 * operator (NOT, ITE, etc) */
75 Node exp_sop_n
= Node::fromExpr(
76 smt::currentSmtEngine()->expandDefinitions(cons
.getSygusOp()));
77 d_ops
.push_back(Rewriter::rewrite(exp_sop_n
));
78 Trace("sygus-grammar-normalize-defs")
79 << "\tOriginal op: " << cons
.getSygusOp()
80 << "\n\tExpanded one: " << exp_sop_n
81 << "\n\tRewritten one: " << d_ops
.back() << "\n\n";
82 d_cons_names
.push_back(cons
.getName());
83 d_pc
.push_back(cons
.getSygusPrintCallback());
84 d_weight
.push_back(cons
.getWeight());
85 d_cons_args_t
.push_back(std::vector
<Type
>());
86 for (const DatatypeConstructorArg
& arg
: cons
)
88 /* Collect unresolved type nodes corresponding to the typenode of the
90 d_cons_args_t
.back().push_back(
92 ->normalizeSygusRec(TypeNode::fromType(
93 static_cast<SelectorType
>(arg
.getType()).getRangeType()))
98 void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm
* sygus_norm
,
101 /* Use the sygus type to not lose reference to the original types (Bool,
103 d_dt
.setSygus(dt
.getSygusType(),
104 sygus_norm
->d_sygus_vars
.toExpr(),
105 dt
.getSygusAllowConst(),
106 dt
.getSygusAllowAll());
107 for (unsigned i
= 0, size_d_ops
= d_ops
.size(); i
< size_d_ops
; ++i
)
109 d_dt
.addSygusConstructor(d_ops
[i
].toExpr(),
115 Trace("sygus-grammar-normalize") << "...built datatype " << d_dt
<< " ";
116 /* Add to global accumulators */
117 sygus_norm
->d_dt_all
.push_back(d_dt
);
118 sygus_norm
->d_unres_t_all
.insert(d_unres_tn
.toType());
119 Trace("sygus-grammar-normalize") << "---------------------------------\n";
122 void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm
* sygus_norm
,
125 std::vector
<unsigned>& op_pos
)
127 std::vector
<unsigned> difference
;
128 std::set_difference(op_pos
.begin(),
130 d_drop_indices
.begin(),
131 d_drop_indices
.end(),
132 std::back_inserter(difference
));
136 /* TODO #1304: have more operators and types. Moreover, have more general ways
137 of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
138 function should realize that it is chainable for integers */
139 bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn
, Node op
)
141 /* Checks whether operator occurs chainable for its type */
142 if (tn
.isInteger() && NodeManager::currentNM()->operatorToKind(op
) == PLUS
)
149 /* TODO #1304: have more operators and types. Moreover, have more general ways
150 of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
151 function should realize that it is chainable for integers */
152 bool SygusGrammarNorm::TransfChain::isId(TypeNode tn
, Node op
, Node n
)
154 if (tn
.isInteger() && NodeManager::currentNM()->operatorToKind(op
) == PLUS
155 && n
== TermUtil::mkTypeValue(tn
, 0))
162 void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm
* sygus_norm
,
165 std::vector
<unsigned>& op_pos
)
167 NodeManager
* nm
= NodeManager::currentNM();
168 std::vector
<unsigned> claimed(d_elem_pos
);
169 claimed
.push_back(d_chain_op_pos
);
170 unsigned nb_op_pos
= op_pos
.size();
171 /* TODO do this properly */
172 /* Remove from op_pos the positions claimed by the transformation */
173 std::sort(op_pos
.begin(), op_pos
.end());
174 std::sort(claimed
.begin(), claimed
.end());
175 std::vector
<unsigned> difference
;
176 std::set_difference(op_pos
.begin(),
180 std::back_inserter(difference
));
182 if (Trace
.isOn("sygus-grammar-normalize-chain"))
184 Trace("sygus-grammar-normalize-chain")
185 << "OP at " << d_chain_op_pos
<< "\n"
186 << d_elem_pos
.size() << " d_elem_pos: ";
187 for (unsigned i
= 0, size
= d_elem_pos
.size(); i
< size
; ++i
)
189 Trace("sygus-grammar-normalize-chain") << d_elem_pos
[i
] << " ";
191 Trace("sygus-grammar-normalize-chain")
193 << op_pos
.size() << " remaining op_pos: ";
194 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
196 Trace("sygus-grammar-normalize-chain") << op_pos
[i
] << " ";
198 Trace("sygus-grammar-normalize-chain") << "\n";
200 /* Build identity operator and empty callback */
202 SygusGrammarNorm::getIdOp(TypeNode::fromType(dt
.getSygusType()));
203 /* If all operators are claimed, create a monomial */
204 if (nb_op_pos
== d_elem_pos
.size() + 1)
206 Trace("sygus-grammar-normalize-chain")
207 << "\tCreating id type for " << d_elem_pos
.back() << "\n";
208 /* creates type for element */
209 std::vector
<unsigned> tmp
;
210 tmp
.push_back(d_elem_pos
.back());
211 Type t
= sygus_norm
->normalizeSygusRec(to
.d_tn
, dt
, tmp
).toType();
212 /* consumes element */
213 d_elem_pos
.pop_back();
214 /* adds to Root: "type" */
215 to
.d_ops
.push_back(iden_op
);
216 to
.d_cons_names
.push_back("id");
217 to
.d_pc
.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
218 /* Identity operators should not increase the size of terms */
219 to
.d_weight
.push_back(0);
220 to
.d_cons_args_t
.push_back(std::vector
<Type
>());
221 to
.d_cons_args_t
.back().push_back(t
);
222 Trace("sygus-grammar-normalize-chain")
223 << "\tAdding " << t
<< " to " << to
.d_unres_tn
<< "\n";
224 /* adds to Root: "type + Root" */
225 to
.d_ops
.push_back(nm
->operatorOf(PLUS
));
226 to
.d_cons_names
.push_back(kindToString(PLUS
));
227 to
.d_pc
.push_back(nullptr);
228 to
.d_weight
.push_back(-1);
229 to
.d_cons_args_t
.push_back(std::vector
<Type
>());
230 to
.d_cons_args_t
.back().push_back(t
);
231 to
.d_cons_args_t
.back().push_back(to
.d_unres_tn
.toType());
232 Trace("sygus-grammar-normalize-chain")
233 << "\tAdding PLUS to " << to
.d_unres_tn
<< " with arg types "
234 << to
.d_unres_tn
<< " and " << t
<< "\n";
236 /* In the initial case if not all operators claimed always creates a next */
237 Assert(nb_op_pos
!= d_elem_pos
.size() + 1 || d_elem_pos
.size() > 1);
238 /* TODO #1304: consider case in which CHAIN op has different types than
240 /* If no more elements to chain, finish */
241 if (d_elem_pos
.size() == 0)
245 /* Creates a type do be added to root representing next step in the chain */
247 d_elem_pos
.push_back(d_chain_op_pos
);
248 if (Trace
.isOn("sygus-grammar-normalize-chain"))
250 Trace("sygus-grammar-normalize-chain")
251 << "\tCreating type for next entry with sygus_ops ";
252 for (unsigned i
= 0, size
= d_elem_pos
.size(); i
< size
; ++i
)
254 Trace("sygus-grammar-normalize-chain")
255 << dt
[d_elem_pos
[i
]].getSygusOp() << " ";
257 Trace("sygus-grammar-normalize-chain") << "\n";
259 /* adds to Root: (\lambda x. x ) Next */
260 to
.d_ops
.push_back(iden_op
);
261 to
.d_cons_names
.push_back("id_next");
262 to
.d_pc
.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
263 to
.d_weight
.push_back(0);
264 to
.d_cons_args_t
.push_back(std::vector
<Type
>());
265 to
.d_cons_args_t
.back().push_back(
266 sygus_norm
->normalizeSygusRec(to
.d_tn
, dt
, d_elem_pos
).toType());
269 std::map
<TypeNode
, Node
> SygusGrammarNorm::d_tn_to_id
= {};
271 /* Traverse the constructors of dt according to the positions in op_pos. Collect
272 * those that fit the kinds established by to_collect. Remove collected operator
273 * positions from op_pos. Accumulate collected positions in collected
275 * returns true if collected anything
277 std::unique_ptr
<SygusGrammarNorm::Transf
> SygusGrammarNorm::inferTransf(
278 TypeNode tn
, const Datatype
& dt
, const std::vector
<unsigned>& op_pos
)
280 NodeManager
* nm
= NodeManager::currentNM();
281 TypeNode sygus_tn
= TypeNode::fromType(dt
.getSygusType());
282 Trace("sygus-gnorm") << "Infer transf for " << dt
.getName() << "..."
284 Trace("sygus-gnorm") << " #cons = " << op_pos
.size() << " / "
285 << dt
.getNumConstructors() << std::endl
;
286 // look for redundant constructors to drop
287 if (options::sygusMinGrammar() && dt
.getNumConstructors() == op_pos
.size())
289 SygusRedundantCons src
;
290 src
.initialize(d_qe
, tn
);
291 std::vector
<unsigned> rindices
;
292 src
.getRedundant(rindices
);
293 if (!rindices
.empty())
295 Trace("sygus-gnorm") << "...drop transf, " << rindices
.size() << "/"
296 << op_pos
.size() << " constructors." << std::endl
;
297 Assert(rindices
.size() < op_pos
.size());
298 return std::unique_ptr
<Transf
>(new TransfDrop(rindices
));
302 // if normalization option is not enabled, we do not infer the transformations
304 if (!options::sygusGrammarNorm())
309 /* TODO #1304: step 1: look for singleton */
310 /* step 2: look for chain */
311 unsigned chain_op_pos
= dt
.getNumConstructors();
312 std::vector
<unsigned> elem_pos
;
313 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
315 Assert(op_pos
[i
] < dt
.getNumConstructors());
316 Expr sop
= dt
[op_pos
[i
]].getSygusOp();
317 /* Collects a chainable operator such as PLUS */
318 if (sop
.getKind() == BUILTIN
319 && TransfChain::isChainable(sygus_tn
, Node::fromExpr(sop
)))
321 Assert(nm
->operatorToKind(Node::fromExpr(sop
)) == PLUS
);
322 /* TODO #1304: be robust for this case */
323 /* For now only transforms applications whose arguments have the same type
325 bool same_type_plus
= true;
326 for (const DatatypeConstructorArg
& arg
: dt
[op_pos
[i
]])
328 if (TypeNode::fromType(
329 static_cast<SelectorType
>(arg
.getType()).getRangeType())
332 same_type_plus
= false;
338 Trace("sygus-grammar-normalize-infer")
339 << "\tFor OP " << PLUS
<< " did not collecting sop " << sop
340 << " in position " << op_pos
[i
] << "\n";
343 Assert(chain_op_pos
== dt
.getNumConstructors());
344 Trace("sygus-grammar-normalize-infer")
345 << "\tCollecting chainable OP " << sop
<< " in position " << op_pos
[i
]
347 chain_op_pos
= op_pos
[i
];
350 /* TODO #1304: check this for each operator */
351 /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
352 if (!TransfChain::isId(sygus_tn
, nm
->operatorOf(PLUS
), Node::fromExpr(sop
)))
354 Trace("sygus-grammar-normalize-infer")
355 << "\tCollecting for NON_ID_ELEMS the sop " << sop
356 << " in position " << op_pos
[i
] << "\n";
357 elem_pos
.push_back(op_pos
[i
]);
360 /* Typenode admits a chain transformation for normalization */
361 if (chain_op_pos
!= dt
.getNumConstructors() && !elem_pos
.empty())
363 Trace("sygus-gnorm") << "...chain transf." << std::endl
;
364 Trace("sygus-grammar-normalize-infer")
365 << "\tInfering chain transformation\n";
366 return std::unique_ptr
<Transf
>(new TransfChain(chain_op_pos
, elem_pos
));
371 TypeNode
SygusGrammarNorm::normalizeSygusRec(TypeNode tn
,
373 std::vector
<unsigned>& op_pos
)
375 /* Corresponding type node to tn with the given operator positions. To be
376 * retrieved (if cached) or defined (otherwise) */
378 if (Trace
.isOn("sygus-grammar-normalize-trie"))
380 Trace("sygus-grammar-normalize-trie")
381 << "\tRecursing on " << tn
<< " with op_positions ";
382 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
384 Trace("sygus-grammar-normalize-trie") << op_pos
[i
] << " ";
386 Trace("sygus-grammar-normalize-trie") << "\n";
388 /* Checks if unresolved type already created (and returns) or creates it
389 * (and then proceeds to definition) */
390 std::sort(op_pos
.begin(), op_pos
.end());
391 if (d_tries
[tn
].getOrMakeType(tn
, unres_tn
, op_pos
))
393 if (Trace
.isOn("sygus-grammar-normalize-trie"))
395 Trace("sygus-grammar-normalize-trie")
396 << "\tTypenode " << tn
<< " has already been normalized with op_pos ";
397 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
399 Trace("sygus-grammar-normalize-trie") << op_pos
[i
] << " ";
401 Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn
<< "\n";
405 if (Trace
.isOn("sygus-grammar-normalize-trie"))
407 Trace("sygus-grammar-normalize-trie")
408 << "\tTypenode " << tn
<< " not yet normalized with op_pos ";
409 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
411 Trace("sygus-grammar-normalize-trie") << op_pos
[i
] << " ";
413 Trace("sygus-grammar-normalize-trie") << "\n";
415 /* Creates type object for normalization */
416 TypeObject
to(tn
, unres_tn
);
418 /* Determine normalization transformation based on sygus type and given
420 std::unique_ptr
<Transf
> transformation
= inferTransf(tn
, dt
, op_pos
);
421 /* If a transformation was selected, apply it */
422 if (transformation
!= nullptr)
424 transformation
->buildType(this, to
, dt
, op_pos
);
427 /* Remaining operators are rebuilt as they are */
428 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
430 Assert(op_pos
[i
] < dt
.getNumConstructors());
431 to
.addConsInfo(this, dt
[op_pos
[i
]]);
433 /* Build normalize datatype */
434 if (Trace
.isOn("sygus-grammar-normalize"))
436 Trace("sygus-grammar-normalize") << "\nFor positions ";
437 for (unsigned i
= 0, size
= op_pos
.size(); i
< size
; ++i
)
439 Trace("sygus-grammar-normalize") << op_pos
[i
] << " ";
441 Trace("sygus-grammar-normalize") << " and datatype " << dt
<< " \n";
443 to
.buildDatatype(this, dt
);
444 return to
.d_unres_tn
;
447 TypeNode
SygusGrammarNorm::normalizeSygusRec(TypeNode tn
)
449 /* Collect all operators for normalization */
450 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
451 std::vector
<unsigned> op_pos(dt
.getNumConstructors());
452 std::iota(op_pos
.begin(), op_pos
.end(), 0);
453 return normalizeSygusRec(tn
, dt
, op_pos
);
456 TypeNode
SygusGrammarNorm::normalizeSygusType(TypeNode tn
, Node sygus_vars
)
458 /* Normalize all types in tn */
459 d_sygus_vars
= sygus_vars
;
460 normalizeSygusRec(tn
);
461 /* Resolve created types */
462 Assert(!d_dt_all
.empty() && !d_unres_t_all
.empty());
463 if (Trace
.isOn("sygus-grammar-normalize-build"))
465 Trace("sygus-grammar-normalize-build")
466 << "making mutual datatyes with datatypes \n";
467 for (unsigned i
= 0, size
= d_dt_all
.size(); i
< size
; ++i
)
469 Trace("sygus-grammar-normalize-build") << d_dt_all
[i
];
471 Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
472 for (const Type
& unres_t
: d_unres_t_all
)
474 Trace("sygus-grammar-normalize-build") << unres_t
<< " ";
476 Trace("sygus-grammar-normalize-build") << "\n";
478 Assert(d_dt_all
.size() == d_unres_t_all
.size());
479 std::vector
<DatatypeType
> types
=
480 NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
481 d_dt_all
, d_unres_t_all
);
482 Assert(types
.size() == d_dt_all
.size());
483 /* Clear accumulators */
485 d_unres_t_all
.clear();
486 /* By construction the normalized type node will be the last one considered */
487 return TypeNode::fromType(types
.back());
490 } // namespace quantifiers
491 } // namespace theory