Z3 Maximize in C++
c, c++, z3
Solution
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.
Problem
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.