From 6625f7a749dac7d2297336978515e0dbb954e9b2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 9 Nov 2015 13:19:10 +0000 Subject: [PATCH] Added Z3_solver_translate to ML API. --- src/api/ml/z3.ml | 7 +++++-- src/api/ml/z3.mli | 3 +++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 9de20e29f..7aa28b272 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -2740,10 +2740,13 @@ struct mk_solver ctx (Some (Symbol.mk_string ctx logic)) let mk_simple_solver ( ctx : context ) = - (create ctx (Z3native.mk_simple_solver (context_gno ctx))) + create ctx (Z3native.mk_simple_solver (context_gno ctx)) let mk_solver_t ( ctx : context ) ( t : Tactic.tactic ) = - (create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t))) + create ctx (Z3native.mk_solver_from_tactic (context_gno ctx) (z3obj_gno t)) + + let translate ( x : solver ) ( to_ctx : context ) = + create to_ctx (Z3native.solver_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx)) let to_string ( x : solver ) = Z3native.solver_to_string (z3obj_gnc x) (z3obj_gno x) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 32ca24128..83c7b66a7 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3122,6 +3122,9 @@ sig The solver supports the commands [Push] and [Pop], but it will always solve each check from scratch. *) val mk_solver_t : context -> Tactic.tactic -> solver + + (** Create a clone of the current solver with respect to a context. *) + val translate : solver -> context -> solver (** A string representation of the solver. *) val to_string : solver -> string