ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003)

Z3Prover · Apr 27, 2022 · 99e299b · 99e299b
1 parent 02d6f6a
commit 99e299b
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
@@ -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)