How to obtain objective from optimize context?

[MohamedElgharbawy]

I am currently calling Z3_optimize_from_string, and I see in the docs that it should:

Add the parsed constraints and objectives to the optimization context.

However, I cannot seem to find what properties of the optimization context contain this information. Does anyone know where I can find this?

[NikolajBjorner]

For the C API, take a look at

z3/src/api/z3_optimization.h

Line 340 in af2cc46

/**

There are two functions:

1. one function retrieves assertions
2. the other function retrieves objectives as a vector of expressions. Soft constraints are converted into a summation (+ (ite a 0 1) (ite b 0 1) ....)

[NikolajBjorner]

AstVectorObj is a python object. It contains iterators already and random access get).
There are several examples in the python directory. you can also [t for t in opt.objectives()] to get a list.

[NikolajBjorner]

there is also help(AstVector) from python

[NikolajBjorner]

You don't call the C API directly from python. You should call the python functions.

[MohamedElgharbawy]

Then does there exist a python function for the C API's Z3_optimize_get_objectives? I could not find one.

[wintersteiger]

Optimize::objectives()?