You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I'm a bit confused about the difference between context and solvers, and how they interact with parsing SMTLIB commands.
From my understanding, the context is going to manage declarations of terms, sorts, etc. while the solver will manage assertions.
Now say using the C API I create a new context with Z3_mk_context. I can directly evaluate SMTLIB commands using Z3_eval_smtlib2_string, although I haven't created any solver yet. Does that mean a default solver is automatically created when a context is ? In that case, how do I get a reference to that solver ?
Now let's say I create a new solver in my context using Z3_mk_solver. If I evaluate new SMTLIB commands using Z3_eval_smtlib2_string (which doesn't take any solver as argument, only the context), will the commands be processed by this new solver ?
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
-
I'm a bit confused about the difference between context and solvers, and how they interact with parsing SMTLIB commands.
From my understanding, the context is going to manage declarations of terms, sorts, etc. while the solver will manage assertions.
Now say using the C API I create a new context with
Z3_mk_context
. I can directly evaluate SMTLIB commands usingZ3_eval_smtlib2_string
, although I haven't created any solver yet. Does that mean a default solver is automatically created when a context is ? In that case, how do I get a reference to that solver ?Now let's say I create a new solver in my context using
Z3_mk_solver
. If I evaluate new SMTLIB commands usingZ3_eval_smtlib2_string
(which doesn't take any solver as argument, only the context), will the commands be processed by this new solver ?Beta Was this translation helpful? Give feedback.
All reactions