From 8a33391708b282f93d0418ea0235f56a1e6fd265 Mon Sep 17 00:00:00 2001 From: Marc Mosko Date: Tue, 6 Jul 2021 01:22:00 -0700 Subject: [PATCH] Expose optimize.assertAndTrack to Java (#5387) Co-authored-by: Marc Mosko --- 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 741dd08d9..c5a26b439 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -73,6 +73,28 @@ public class Optimize extends Z3Object { 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 constraint, Expr p) + { + getContext().checkContextMatch(constraint); + getContext().checkContextMatch(p); + + Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(), + constraint.getNativeObject(), p.getNativeObject()); + } + /** * Handle to objectives returned by objective functions. **/