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 constraints) Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); } } + + /// + /// Assert a constraint into the optimize solver, and track it (in the unsat) core + /// using the Boolean constant p. + /// + /// + /// This API is an alternative to 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 + /// and the Boolean literals + /// provided using with assumptions. + /// + 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); + } + /// /// Handle to objectives returned by objective functions. ///