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

change Z3_get_decl_kind API to correctly identify OP_B*_I and OP_B*_NO_OVFL instead of returning Z3_OP_UNINTERPRETED

Browse source
This commit is contained in:
Nuno Lopes 2016-05-11 14:30:37 +01:00
parent f8795f3522
commit d30ba3f1ad
2 changed files with 17 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_ast.cpp
View file

@ -1066,15 +1066,14 @@ extern "C" {
case OP_BV2INT: return Z3_OP_BV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BSMUL_NO_OVFL:
case OP_BUMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
case OP_BSDIV_I:
case OP_BUDIV_I:
case OP_BSREM_I:
case OP_BUREM_I:
case OP_BSMOD_I:
return Z3_OP_UNINTERPRETED;
case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: return Z3_OP_BSREM_I;
case OP_BUREM_I: return Z3_OP_BUREM_I;
case OP_BSMOD_I: return Z3_OP_BSMOD_I;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;

9
src/api/z3_api.h
View file

@ -1060,6 +1060,15 @@ typedef enum {
Z3_OP_CARRY,
Z3_OP_XOR3,
Z3_OP_BSMUL_NO_OVFL,
Z3_OP_BUMUL_NO_OVFL,
Z3_OP_BSMUL_NO_UDFL,
Z3_OP_BSDIV_I,
Z3_OP_BUDIV_I,
Z3_OP_BSREM_I,
Z3_OP_BUREM_I,
Z3_OP_BSMOD_I,
// Proofs
Z3_OP_PR_UNDEF = 0x500,
Z3_OP_PR_TRUE,