mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge pull request #597 from nunoplopes/master

Browse source 
change Z3_get_decl_kind API to correctly identify OP_B*_I and OP_B*_NO_OVFL instead of returning Z3_OP_UNINTERPRETED
This commit is contained in:
Christoph M. Wintersteiger 2016-05-12 18:36:14 +01:00
parent 0ddf2d92fe d30ba3f1ad
commit b0bd848a27
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_BV2INT: return Z3_OP_BV2INT;
case OP_CARRY: return Z3_OP_CARRY; case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3; case OP_XOR3: return Z3_OP_XOR3;
case OP_BSMUL_NO_OVFL: case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
case OP_BUMUL_NO_OVFL: case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
case OP_BSMUL_NO_UDFL: case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
case OP_BSDIV_I: case OP_BSDIV_I: return Z3_OP_BSDIV_I;
case OP_BUDIV_I: case OP_BUDIV_I: return Z3_OP_BUDIV_I;
case OP_BSREM_I: case OP_BSREM_I: return Z3_OP_BSREM_I;
case OP_BUREM_I: case OP_BUREM_I: return Z3_OP_BUREM_I;
case OP_BSMOD_I: case OP_BSMOD_I: return Z3_OP_BSMOD_I;
return Z3_OP_UNINTERPRETED;
default: default:
UNREACHABLE(); UNREACHABLE();
return Z3_OP_UNINTERPRETED; return Z3_OP_UNINTERPRETED;

9
src/api/z3_api.h
View file

@ -1060,6 +1060,15 @@ typedef enum {
Z3_OP_CARRY, Z3_OP_CARRY,
Z3_OP_XOR3, 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 // Proofs
Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_UNDEF = 0x500,
Z3_OP_PR_TRUE, Z3_OP_PR_TRUE,