how to set opt.strategy in z3py?

[taineleau]

how to set opt.strategy in z3py?

 -opt.strategy=STR
          Sets the optimization search strategy: 
           - lin : linear search (default)
           - bin : binary search
           - ada : adaptive search
          A lower bound is required to minimize an objective with bin/ada 
          search strategy. Dual for maximization. 

[LeventErkok]

NB. These quiestions are better suited for the stack-overflow z3py group: https://stackoverflow.com/questions/tagged/z3

Long story short, you use the syntax:

   set_option('smt.mbqi.id', 'my_id')

So, for your example, it'd be something like:

   set_option('opt.strategy', 'lin')

But latest z3 complains:

WARNING: unknown parameter 'strategy' at module 'opt'
Legal parameters are:
...

So, I'm guessing you must've an older(?) version of z3 that supported this parameter. It doesn't seem to be supported any longer.

[NikolajBjorner]

Thanks, yes StackOverflow is designed for questions of this form. GitHub issues are better suited for tracking bugs.

Maybe it is a different tool that uses this naming convention. It was not used for Z3. Here are the options:

C:\z3\release>z3 /pm:opt
[module] opt, description: optimization parameters
    dump_benchmarks (bool) dump benchmarks for profiling (default: false)
    dump_models (bool) display intermediary models to stdout (default: false)
    elim_01 (bool) eliminate 01 variables (default: true)
    enable_sat (bool) enable the new SAT core for propositional constraints (default: true)
    enable_sls (bool) enable SLS tuning during weighted maxsast (default: false)
    maxlex.enable (bool) enable maxlex heuristic for lexicographic MaxSAT problems (default: true)
    maxres.add_upper_bound_block (bool) restict upper bound with constraint (default: false)
    maxres.hill_climb (bool) give preference for large weight cores (default: true)
    maxres.max_core_size (unsigned int) break batch of generated cores if size reaches this number (default: 3)
    maxres.max_correction_set_size (unsigned int) allow generating correction set constraints up to maximal size (default: 3)
    maxres.max_num_cores (unsigned int) maximal number of cores per round (default: 4294967295)
    maxres.maximize_assignment (bool) find an MSS/MCS to improve current assignment (default: false)
    maxres.pivot_on_correction_set (bool) reduce soft constraints if the current correction set is smaller than current core (default: true)
    maxres.wmax (bool) use weighted theory solver to constrain upper bounds (default: false)
    maxsat_engine (symbol) select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres' (default: maxres)
    optsmt_engine (symbol) select optimization engine: 'basic', 'symba' (default: basic)
    pb.compile_equality (bool) compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) (default: false)
    pp.neat (bool) use neat (as opposed to less readable, but faster) pretty printer when displaying context (default: true)
    priority (symbol) select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box' (default: lex)
    rlimit (unsigned int) resource limit (0 means no limit) (default: 0)
    solution_prefix (symbol) path prefix to dump intermediary, but non-optimal, solutions (default: )
    timeout (unsigned int) timeout (in milliseconds) (UINT_MAX and 0 mean no timeout) (default: 4294967295)

Only symba and default are available at this point. Some other options were kicked out some time ago.