search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Objective function is not supported #167

Closed august782 closed 9 years ago

august782 commented 9 years ago

I'm trying to use Z3 to find the optimal model for a set of formulas that relies on converting booleans to integers and multiplying these results with other arithmetic expressions. The formula I tried through the Z3Opt web interface is at:

http://rise4fun.com/Z3Opt/ISH

When I run it through the interface I get "Objective function ... is not supported"

Is this formulation something Z3 can accept?

NikolajBjorner commented 9 years ago

The formulation is a non-linear expression over finite domain variables. Z3 does not fully support non-linear optimization and in this case determines that it cannot support this constraint. You can turn it into a linear function by distributing over multiplication. E.g., http://rise4fun.com/Z3Opt/plkO