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

expose extra symbols for logic ALL, requested in #1364

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-25 12:03:47 -08:00
parent 441c0de3c8
commit 1c5f798cbe
4 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/bv_decl_plugin.cpp
View file

@ -670,7 +670,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const {
}
void bv_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
if (logic == symbol::null)
if (logic == symbol::null || logic == symbol("ALL"))
sort_names.push_back(builtin_name("bv", BV_SORT));
sort_names.push_back(builtin_name("BitVec", BV_SORT));
}
@ -717,7 +717,7 @@ 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));
if (logic == symbol::null) {
if (logic == symbol::null || logic == symbol("ALL")) {
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));