Programmatic setting of options/parameters #7367
Unanswered
ThomasHaas
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Z3 seems to provide parameters on different levels: global, context, and solver.
From the documentation, it seems that setting options on the global level will simply cause all generated contexts to inherit those options (unless explicity overwritten).
My questions are now:
(1) Is the same true for solvers that are generated from a context, i.e., can solver options be set on the context level such that solvers working over that context inherit the options?
(2) If the answer to (1) is no: Are all solver options set via Z3_solver_set_params or are there other means to do so?
(3) Does Z3_solver_set_params, when called with a single parameter, only update that single parameter or also reset the unspecified parameters to some default? I.e., can one call this function multiple times to incrementally set the options?
(4) Is there a way to set solver options purely based on strings, avoiding the type-safe functions of parameter sets?
(5) If a user propagator wants to update options mid-solving, what API has to be used? For example, how does one set
smt.up.persist_clauses=true
during solving?Beta Was this translation helpful? Give feedback.
All reactions