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

ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003)

Browse source
This commit is contained in:
Ryan Goulden 2022-04-27 03:36:09 -07:00 committed by GitHub
parent 02d6f6a613
commit 99e299b90c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -119,6 +119,7 @@ sig
val get_ast_kind : ast -> Z3enums.ast_kind
val is_expr : ast -> bool
val is_app : ast -> bool
val is_numeral : ast -> bool
val is_var : ast -> bool
val is_quantifier : ast -> bool
val is_sort : ast -> bool
@ -191,6 +192,7 @@ end = struct
| _ -> false
let is_app (x:ast) = get_ast_kind x = APP_AST
let is_numeral (x:ast) = get_ast_kind x = NUMERAL_AST
let is_var (x:ast) = get_ast_kind x = VAR_AST
let is_quantifier (x:ast) = get_ast_kind x = QUANTIFIER_AST
let is_sort (x:ast) = get_ast_kind x = SORT_AST
@ -1018,7 +1020,7 @@ struct
let is_int (x:expr) =
((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = INT_SORT)
let is_arithmetic_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ANUM)
let is_arithmetic_numeral (x:expr) = (AST.is_numeral x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_ANUM)
let is_le (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LE)
let is_ge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_GE)
let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_LT)
@ -1129,7 +1131,7 @@ struct
let mk_sort (ctx:context) size = Z3native.mk_bv_sort ctx size
let is_bv (x:expr) =
((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) = BV_SORT)
let is_bv_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNUM)
let is_bv_numeral (x:expr) = (AST.is_numeral x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNUM)
let is_bv_bit1 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT1)
let is_bv_bit0 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BIT0)
let is_bv_uminus (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_BNEG)