ML API: added Expr.equal and Expr.compare

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/api/ml/z3.ml

@@ -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

src/api/ml/z3.mli

@@ -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 *)