From 99e299b90c474613f083dd6d393ac7129f8a2f95 Mon Sep 17 00:00:00 2001 From: Ryan Goulden Date: Wed, 27 Apr 2022 03:36:09 -0700 Subject: [PATCH] ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003) --- src/api/ml/z3.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index b904937a946..b551688c562 100644 --- 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)