What is the equivalent of check-sat-using in z3py?

Question

I've been trying to achieve the exact same goal as this post. Z3 randomness of generated model values

Except, the answer is in smt, how do I use the check-sat-using in z3py in python? Can someone please help me translate this code into python code?

(set-option :smt.arith.random_initial_value true)
(declare-const x Int)
(declare-const y Int)
(assert (> (+ x y) 0))
(check-sat-using (using-params qflra :random_seed 1))
(get-model)
(check-sat-using (using-params qflra :random_seed 2))
(get-model)
(check-sat-using (using-params qflra :random_seed 3))
(get-model)

alias · Accepted Answer · 2020-02-04T17:31:56.027

In the SMTLib interface, check-sat-using is a way of telling z3 which tactics to use. When you use z3py, you directly use the tactic language and explicitly create solvers. So, in a sense, there is no corresponding call in z3py to check-sat-using. Instead, you get an entire tactic language, which is much more flexible and powerful.

For examples see: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

Note also that check-sat-using combines tactics and settings in a sense, in z3py you use set_param to achive parameter settings, and the tactic language to express what strategy you want to use.

As a general rule of thumb, do not try to "translate" between SMTLib and Z3 Python interfaces. While both can express same queries, the programming model is different and trying to translate "command-by-command" would lead you to non-idiomatic and hard-to-maintain code. Instead, if you want to use Z3py, simply learn how things are done there, keeping in mind they can look quite different from the SMTLib land. This is a great resource to read through to get you started: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/

What is the equivalent of check-sat-using in z3py?

1 Answers1