mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

removing tabs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-22 16:58:26 -08:00
parent 54e8612f4d
commit 5262e1986c
1 changed files with 455 additions and 457 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/ml/z3.ml
View file

@ -807,15 +807,15 @@ end = struct
let gno e = match e with Expr(a) -> (z3obj_gno a) let gno e = match e with Expr(a) -> (z3obj_gno a)
let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no ->
let e = z3_native_object_of_ast_ptr ctx no in
if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then
Expr(z3_native_object_of_ast_ptr ctx no) Expr(e)
else else
let s = Z3native.get_sort (context_gno ctx) no in let s = Z3native.get_sort (context_gno ctx) no in
let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in
if (Z3native.is_algebraic_number (context_gno ctx) no) then if (Z3native.is_algebraic_number (context_gno ctx) no) then
Expr(z3_native_object_of_ast_ptr ctx no) Expr(e)
else else if (Z3native.is_numeral_ast (context_gno ctx) no) then
if (Z3native.is_numeral_ast (context_gno ctx) no) then
match sk with match sk with
| REAL_SORT | REAL_SORT
| BOOL_SORT | BOOL_SORT
@ -827,12 +827,10 @@ end = struct
| FLOATING_POINT_SORT | FLOATING_POINT_SORT
| INT_SORT | INT_SORT
| DATATYPE_SORT | DATATYPE_SORT
| FINITE_DOMAIN_SORT -> | FINITE_DOMAIN_SORT -> Expr(e)
Expr(z3_native_object_of_ast_ptr ctx no) | _ -> raise (Z3native.Exception "Unsupported numeral object")
| _ ->
raise (Z3native.Exception "Unsupported numeral object")
else else
Expr(z3_native_object_of_ast_ptr ctx no) Expr(e)
let expr_of_ast a = let expr_of_ast a =
let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in