mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-28 12:56:28 +00:00
Code Activity

recognize ubv_to_int as part of BV logic

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-27 13:08:54 -07:00
parent 51da9db615
commit 5fe4d88d43
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/bv_decl_plugin.cpp
View file

@ -783,6 +783,9 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT));
op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
op_names.push_back(builtin_name("bit2bool", OP_BIT2BOOL));
op_names.push_back(builtin_name("ubv_to_int", OP_UBV2INT));
op_names.push_back(builtin_name("sbv_to_int", OP_SBV2INT));
op_names.push_back(builtin_name("int_to_bv", OP_INT2BV));
if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD" || logic == "HORN") {
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
@ -804,11 +807,10 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
op_names.push_back(builtin_name("int2bv",OP_INT2BV));
op_names.push_back(builtin_name("int_to_bv",OP_INT2BV));
op_names.push_back(builtin_name("bv2int",OP_UBV2INT));
op_names.push_back(builtin_name("bv2nat",OP_UBV2INT));
op_names.push_back(builtin_name("ubv_to_int",OP_UBV2INT));
op_names.push_back(builtin_name("sbv_to_int",OP_SBV2INT));
op_names.push_back(builtin_name("mkbv",OP_MKBV));
}
}