Z3 Maximize in C++

Question

In Z3, the following is clearly evaluated to a maximum of 2, with the model x=true and y=true.

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert(= z false))
(maximize(
  +  
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0)
  )
)
(check-sat)
(get-model)

How could I implement this using the C/C++ APIs? I've tried simply parsing using this:

Z3_ast parsed = Z3_parse_smtlib2_string(c,<The above Z3>,0,0,0,0,0,0);
z3::expr simpleExample(c, parsed);
s.add(simpleExample);

But it prints "unsupported \n ;maximize".

I wouldn't mind constructing the expression manually - rather than using a constructed file. I simply didn't know which expr functions or operators to use for "maximize".

ADDENDUM: In light of some recent answers and discussions, it seems clear that what I am requesting is not normal functionality at the moment. So, I alter the question to ask for the specific details of a way to make this work as things stand at the moment.

Chalfant

Alternative: Does MS provide the source code for Z3? If so you could debug the first approach which is correctly parsed and evaluated. – Quillet

I'm not sure that they do. I do know however that my example works on their website. – Jubal

z3.codeplex.com/SourceControl/latest#README – Quillet

I see, but I'm not really seeing your point. What precisely are you suggesting? – Jubal

Grab the source. Build it, run and debug your code. You could debug when the token parser consumes maximize and check why it chokes on "unsupported ..." . You will see the fail condition for that and you might gain some insight. Alternatively you could browse the source and check what internal representation maximize requires and how you should reformat your code. – Quillet

@Quillet Good idea. I'll do that if it comes to it. Apparently we are sort of pushing the boundaries of what they are up to implementing - and exposing to the APIs. – Jubal

Answer 1

Thanks for pointing out this issue. The optimization features are not part of SMT-LIB2. They are custom extensions. Also, the function that parses SMT-LIB2 benchmarks does not have any way to reflect back the optimization pragmas. The reason why the API parser does not recognize these extensions is that the optimization features are not registered with that parser (they are registered with the command-line parser). Of course they are not registered with the parser in the "unstable" branch, and they are also not registered with the parser in the "opt" branch that contains the optimization extensions. I was almost tempted to "fix" this, based on your post, but I am now not sure why it would be useful since that parser has no way of using those extensions. Z3 has other extensions that are also not exposed for the SMT-LIB2 parser. So for now, I am inclined to keep the parser exposed by the API to only accept proper SMT-LIB2.

Note that Christoph points out that the optimization features are only part of an "opt" branch. You are welcome to try it out, but it is still churning quite a bit. The API is as far as I am concerned "feature complete" (to answer (1)). You can use it from Python, Java and .NET. The OCaml integration is pending other changes to OCaml APIs. I have not had an opportunity to provide any extensive documentation for the APIs, but there is a short tutorial for the SMT-LIB extensions on http://rise4fun.com/Z3/tutorial/optimization.

Crag

Answer 2

The optimization features in Z3 are under heavy construction in the `opt' branch and not integrated with the unstable or master branches. It's quite possible that not all the functionality has been added to the API yet. See also Nikolaj's answers to these questions:

Encoding “at-most-k / at-least-k booleans are true” constraints in Z3

Simplex in z3 via for-all

Ree

Thank you kindly. A couple of questions. 1) You say "it's quite possible..." is there some way we could make ourselves more certain of this? 2) Can we build and use this 'opt' branch "at home" (by the way the last commits are not all that recent)? 3) So is there any way, using any language, or any platform (Windows/Linux) to get that Z3 input shown in the question to run outside of using the website? Millionen Dank – Jubal

Hi again, I just downloaded and tried the 'opti' branch. The command line Z3 still didn't pick up the 'maximize' condition. Inside the code I saw some rather cryptic-looking functions with names like "z3_check_opti". I presume these are related to this problem, but it is really too unclear for me to make use of this. Do you have any ideas? – Jubal

1) Yes. 2) Yes. 3) Yes, but no convenient one. Some things take longer than a week to implement. – Ree

@Chalfant I believe Nikolaj Bjorner refers to the opt- branch, which is quite different from the opti- branch. The maximization in the opti- branch is exposing inner interface for the SYMBA maximization tool and is the different story altogether. – Recent