From b0fef6429fb29a33eb14adf9a61353b59f0f7fd0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 26 Oct 2024 01:33:09 -0700
Subject: [PATCH] Add assert_and_track support to Optimize class in .NET
 binding (#7437)

Related to #7436

#7436

---

For more details, open the [Copilot Workspace session](https://copilot-workspace.githubnext.com/Z3Prover/z3/issues/7436?shareId=XXXX-XXXX-XXXX-XXXX).
---
 src/api/dotnet/Optimize.cs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 891ed4105e1..3bc06de161f 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -148,6 +148,28 @@ private void AddConstraints(IEnumerable<BoolExpr> constraints)
                 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
             }
         }
+
+        /// <summary>
+        /// Assert a constraint into the optimize solver, and track it (in the unsat) core 
+        /// using the Boolean constant p. 
+        /// </summary>
+        /// <remarks>
+        /// This API is an alternative to <see cref="Check(Expr[])"/> 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(BoolExpr[],BoolExpr[])"/> 
+        /// and the Boolean literals
+        /// provided using <see cref="Check(Expr[])"/> with assumptions.
+        /// </remarks>        
+        public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
+        {
+            Debug.Assert(constraint != null);
+            Debug.Assert(p != null);
+            Context.CheckContextMatch(constraint);
+            Context.CheckContextMatch(p);
+                        
+            Native.Z3_optimize_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
+        }
+
         /// <summary>
         /// Handle to objectives returned by objective functions.
         /// </summary>