mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

allow to pass Booleans as arguments to arithmetic expressions

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-31 12:00:54 -08:00
parent 994c7ef52d
commit 6a412f7f04
1 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ast/ast.cpp
View file

@ -27,6 +27,7 @@ Revision History:
#include "ast/ast_util.h"
#include "ast/ast_smt2_pp.h"
#include "ast/array_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_translation.h"
#include "util/z3_version.h"
@ -2131,12 +2132,17 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
expr* ast_manager::coerce_to(expr* e, sort* s) {
sort* se = e->get_sort();
if (s != se && s->get_family_id() == arith_family_id && se->get_family_id() == arith_family_id) {
if (s->get_decl_kind() == REAL_SORT) {
if (s->get_decl_kind() == REAL_SORT)
return mk_app(arith_family_id, OP_TO_REAL, e);
}
else {
return mk_app(arith_family_id, OP_TO_INT, e);
}
else
return mk_app(arith_family_id, OP_TO_INT, e);
}
if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) {
arith_util au(*this);
if (s->get_decl_kind() == REAL_SORT)
return mk_ite(e, au.mk_real(1), au.mk_real(0));
else
return mk_ite(e, au.mk_int(1), au.mk_int(0));
}
else {
return e;