From 689ed9fa12bbf0fc900b2affc77c7160725a550d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:25:52 +0000 Subject: [PATCH] Added Z3_mk_array_ext to ML API. Relates to #292 --- src/api/ml/z3.ml | 3 +++ src/api/ml/z3.mli | 7 +++++++ 2 files changed, 10 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 7aa28b272..ca48a72bf 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1217,6 +1217,9 @@ struct let mk_term_array ( ctx : context ) ( arg : expr ) = expr_of_ptr ctx (Z3native.mk_array_default (context_gno ctx) (Expr.gno arg)) + + let mk_array_ext ( ctx : context) ( arg1 : expr ) ( arg2 : expr ) = + expr_of_ptr ctx (Z3native.mk_array_ext (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e97313148..e69f7f576 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -866,6 +866,13 @@ sig Produces the default range value, for arrays that can be represented as finite maps with a default range value. *) val mk_term_array : context -> Expr.expr -> Expr.expr + + (** Create array extensionality index given two arrays with the same sort. + + The meaning is given by the axiom: + (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B)) *) + val mk_array_ext : context -> Expr.expr -> Expr.expr -> Expr.expr + end (** Functions to manipulate Set expressions *)