mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix convex converter for multi-arity addition

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-19 19:48:09 -07:00
parent e9ad4ab584
commit 0b56440cba
1 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz_qe/pdr_generalizers.cpp
View file

@ -434,9 +434,19 @@ namespace pdr {
if (translate(app->get_decl(), index, result)) {
return true;
}
if (a.is_add(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) {
result = a.mk_add(r1, r2);
return true;
if (a.is_add(term)) {
bool ok = true;
expr_ref_vector args(m);
for (unsigned i = 0; ok && i < app->get_num_args(); ++i) {
ok = mk_convex(app->get_arg(i), index, is_mul, r1);
if (ok) {
args.push_back(r1);
}
}
if (ok) {
result = a.mk_add(args.size(), args.c_ptr());
}
return ok;
}
if (a.is_sub(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) {
result = a.mk_sub(r1, r2);