CODEWITHSUNDEEP
c#.netz3
MrWoffle
MrWoffle

Reputation: 149

Z3 Optimize timeout

I want to set a timeout in z3 so i dont get a optimal solution but one that fits the constraints. I use .Net and tried something like this:

using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) {
    var solver = context.MkSolver(); // i actually want to use MkOptimize() 
    Params p = context.MkParams();
    p.Add("timeout", 1000);
    solver.Parameters = p;
    IntExpr x = context.MkIntConst("x");
    // ...
    solver.Check();
    solver.Model.Evaluate(x);
}

The timeout is working correct but i cant use the so far found solution because solver.Check() is UNKNOWN ...

When i use MkOptimize instead of MkSolver i get a unknown parameter exception

So my question now is how do i get the best solution so far after the timeout and how can i use this with MkOptimize

Upvotes: 1

Views: 210

Answers (1)

alias
alias

Reputation: 30418

I'd very much doubt that you can reliably get a "best-so-far" answer when the solver says Unknown due to timeout or any other reason. Even if you got a model, it wouldn't necessarily satisfy all your constraints at that point. Since this is a very Z3 specific question, you might get better mileage asking at https://github.com/Z3Prover/z3/issues and summarizing the answer you get back over here for the community.

Upvotes: 1

Related Questions