CODEWITHSUNDEEP
c++coptimizationz3
Modass
Modass

Reputation: 197

Z3 optimization: detect unboundedness via API

I am experiencing difficulties in detecting unboundedness of an optimization problem. As stated in the examples and in some answers here, the printed result of an unbounded optimization problem equals to something like "oo", which has to be interpreted (via string compare?).

My question is: Is there any way to use the API to detect this?

I've searched for some time now and the only function, which might do what I want is Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t) which returns some Z3_ast object. The problem is: Is this the right approach and how do I get the unbounded property out of that Z3_ast object?

Upvotes: 1

Views: 80

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is currently no built-in way to extract unbounded values or infinitesimals. The optimization engine uses ad-hoc constants called "epsilon" (of type Real) and "oo" (of type Real or Integer) when representing maximal/minimal that are unbounded or at a strict bound. There is no built-in recognizer for these constants and formally, they don't belong to the domain of Reals. They belong to an extension field. So formally, I would have to return an expression over a different number field or return what amounts to a triple of numerals (epsilon, standard numeral, infinite). For example, a standard numeral 5.6 would be represented as (0, 5.6, 0), and a numeral that comes just below 5.6 is represented as (-1, 5.6, 0), and a numeral that is +infinity is (0, 0, 1). Returning three values instead of one seemed no more satisfactory a solution to me as returning an expression. I am leaving it to users to post-process the expressions that are returned and indeed match for symbols "oo" and "epsilon" to decompose the values if they need so.

Upvotes: 1

Related Questions