mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

Add assert_and_track support to Optimize class in .NET binding (#7437)

Browse source 
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).
This commit is contained in:
Nikolaj Bjorner 2024-10-26 01:33:09 -07:00 • committed by GitHub
parent 8b657f27aa
commit b0fef6429f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/api/dotnet/Optimize.cs
View file

@ -148,6 +148,28 @@ namespace Microsoft.Z3
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>