Reputation: 39
I'm searching for a way to add a minimize/maximize objective to the Z3 solver, using the .NET API. Is there any way?
Upvotes: 3
Views: 347
Reputation: 8369
You can use the method MkOptimize from the Context object to create an Optimize object. You can then add constraints and objective functions to this object. The file Optimize.cs contains these methods: https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/Optimize.cs
There is a tutorial on using the API from F# (which uses the same .NET APIs as C#) on http://lonelypad.blogspot.dk/2014/08/f-and-linear-programming-introduction.html. It is linked from http://rise4fun.com/Z3Opt/tutorial/guide.
Upvotes: 1