mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 10:14:42 +00:00
Code Activity

Fix issue reported at http://z3.codeplex.com/workitem/14

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-24 13:22:28 -08:00
parent 7e7927052e
commit 711abc75fb
5 changed files with 27 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/api/api_numeral.cpp
View file

@ -24,27 +24,27 @@ Revision History:
#include"bv_decl_plugin.h"
#include"algebraic_numbers.h"
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
fid != mk_c(c)->get_bv_fid() &&
fid != mk_c(c)->get_datalog_fid()) {
return false;
}
return true;
}
bool check_numeral_sort(Z3_context c, Z3_sort ty) {
bool is_num = is_numeral_sort(c, ty);
if (!is_num) {
SET_ERROR_CODE(Z3_INVALID_ARG);
}
return is_num;
}
extern "C" {
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
fid != mk_c(c)->get_bv_fid() &&
fid != mk_c(c)->get_datalog_fid()) {
return false;
}
return true;
}
bool check_numeral_sort(Z3_context c, Z3_sort ty) {
bool is_num = is_numeral_sort(c, ty);
if (!is_num) {
SET_ERROR_CODE(Z3_INVALID_ARG);
}
return is_num;
}
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, const char* n, Z3_sort ty) {
Z3_TRY;
LOG_Z3_mk_numeral(c, n, ty);