Marco Oberwittler
Marco Oberwittler

Reputation: 39

Is there a way to use a maximize/ minimize objective with Z3 solver in C#?

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

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

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

Related Questions