From 12631112630f55308eb342a5c12312bac99962be Mon Sep 17 00:00:00 2001
From: Marc Mosko <mmosko@parc.com>
Date: Mon, 5 Jul 2021 19:48:37 -0700
Subject: [PATCH] Expose optimize.assertAndTrack to Java

---
 src/api/java/Optimize.java | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index 741dd08d99d..c5a26b439ac 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -73,6 +73,28 @@ public void Add(Expr<BoolSort> ... constraints)
         Assert(constraints);
     }
 
+    /** 
+     * Assert a constraint into the optimizer, and track it (in the unsat) core
+     * using the Boolean constant p. 
+     * 
+     * Remarks: 
+     * This API is an alternative to {@link #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 {@link #assertAndTrack}
+     * and the Boolean literals
+     * provided using {@link #check} with assumptions.
+     */ 
+    public void AssertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
+    {
+        getContext().checkContextMatch(constraint);
+        getContext().checkContextMatch(p);
+
+        Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
+                constraint.getNativeObject(), p.getNativeObject());
+    }
+
     /**
      * Handle to objectives returned by objective functions.
      **/