3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

ML API: added Expr.equal and Expr.compare

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-23 15:15:59 +01:00
parent a73a66b79c
commit 9160925c28
2 changed files with 16 additions and 2 deletions

View file

@ -717,6 +717,8 @@ sig
val mk_app : context -> FuncDecl.func_decl -> expr list -> expr
val mk_numeral_string : context -> string -> Sort.sort -> expr
val mk_numeral_int : context -> int -> Sort.sort -> expr
val equal : expr -> expr -> bool
val compare : expr -> expr -> int
end = struct
type expr = Expr of AST.ast
@ -830,6 +832,10 @@ end = struct
let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) =
expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty))
let equal ( a : expr ) ( b : expr ) = AST.equal (ast_of_expr a) (ast_of_expr b)
let compare a b = AST.compare (ast_of_expr a) (ast_of_expr b)
end
open FuncDecl

View file

@ -554,9 +554,17 @@ sig
val mk_numeral_string : context -> string -> Sort.sort -> expr
(** Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer.
It is slightly faster than [MakeNumeral] since it is not necessary to parse a string.
@return A Term with the given value and sort *)
It is slightly faster than [MakeNumeral] since it is not necessary to parse a string.
@return A Term with the given value and sort *)
val mk_numeral_int : context -> int -> Sort.sort -> expr
(** Comparison operator.
@return True if the two expr's are equal; false otherwise. *)
val equal : expr -> expr -> bool
(** Object Comparison.
@return Negative if the first expr should be sorted before the second, positive if after, else zero. *)
val compare : expr -> expr -> int
end
(** Boolean expressions; Propositional logic and equality *)