From 3a0af6d15fc7591594cb0aeed5a3eb9e1f2b6a40 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 17 Jan 2013 19:47:51 +0000
Subject: [PATCH] ML API: Added Solver.assert_and_track

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/ml/z3.ml | 38 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 0dfb173c4..f5c3e3d82 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -5159,8 +5159,42 @@ struct
   *)        
   let assert_ ( x : solver ) ( constraints : bool_expr array ) =
     let f e = (Z3native.solver_assert (z3obj_gnc x) (z3obj_gno x) e#gno) in
-    ignore (Array.map f constraints) ;
-    ()
+    ignore (Array.map f constraints)
+
+  (**
+     * Assert multiple constraints (cs) into the solver, and track them (in the
+     * unsat) core
+     * using the Boolean constants in ps.
+     *
+     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * extracting unsat cores.
+     * Both APIs can be used in the same solver. The unsat core will contain a
+     * combination
+     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * and the Boolean literals
+     * provided using <see cref="Check"/> with assumptions.
+  *)
+  let assert_and_track ( x : solver ) ( cs : bool_expr array ) ( ps : bool_expr array ) =
+    if ((Array.length cs) != (Array.length ps)) then
+      raise (Z3native.Exception "Argument size mismatch")
+    else
+      let f i e = (Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) e#gno (Array.get ps i)#gno) in
+      ignore (Array.iteri f cs)
+	
+  (**
+     * Assert a constraint (c) into the solver, and track it (in the unsat) core
+     * using the Boolean constant p.
+     * 
+     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * extracting unsat cores.
+     * Both APIs can be used in the same solver. The unsat core will contain a
+     * combination
+     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * and the Boolean literals
+     * provided using <see cref="Check"/> with assumptions.
+  *)
+  let assert_and_track ( x : solver ) ( c : bool_expr ) ( p : bool_expr ) =    
+    Z3native.solver_assert_and_track (z3obj_gnc x) (z3obj_gno x) c#gno p#gno
 
   (**
      The number of assertions in the solver.