Recent questions tagged z3

0 votes

352 views

1 answer

z3 - y=1/x, x=0 satisfiable in the reals?

In SMT-LIB: (declare-fun y () Real) (declare-fun x () Real) (assert (= 0.0 x)) (assert (= y (/ ... check-sat) Should this model be SAT or UNSAT? See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

400 views

1 answer

z3 - Non-linear arithmetic and uninterpreted functions

(declare-const x Real) (declare-fun f (Real) Real) (assert (= (f 1.0) 0.0)) (assert (= (* x x) ... can handle both at the same time? Thank you. See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

350 views

1 answer

z3 - C API for Quantifiers

I want to solve constraints that contain quantifiers using Z3 C API. I am struggling to use the functions ... anyone help? Thanks. Kaustubh. See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

655 views

1 answer

z3 - Create an array with fixed size and initialize it

I'm going to create an array with fixed size and initialize it with some values. For example, the following C++ ... utilities in Z3 to model it? See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

737 views

1 answer

z3 - Minimum and maximum values of integer variable

Let's assume a very simple constraint: solve(x > 0 && x < 5). Can Z3 (or any other SMT solver, or any ... minimum is 1 and the maximum is 4. See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

364 views

1 answer

z3 - Need help understanding the equation

Have the equation Pell x*x - 193 * y*y = 1 in z3py: x = BitVec('x',64) y = BitVec('y',64) ... answer: [y = 448036604040, x = 6224323426849] See Question&Answers more detail:os...

asked Oct 24, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

404 views

1 answer

z3 - Combining nonlinear Real with linear Int

I've read the posts about nonlinear arithmetic and uninterpreted functions. I'm still very new to SMT world, so ... types that were asserted on? See Question&Answers more detail:os...

asked Oct 17, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

461 views

1 answer

z3 - Z3py: how to get the list of variables from a formula?

In Z3Py, I have a formula. How can I retrieve the list of variables using in the formula? Thanks. See Question&Answers more detail:os...

asked Oct 17, 2021 in Technique[技术] by 深蓝 (71.8m points)

0 votes

750 views

1 answer

z3 - K-out-of-N constraint in Z3Py

I am using the Python bindings for the Z3 theorem prover (Z3Py). I have N boolean variables, x1,.., ... efficient than expressing it manually. See Question&Answers more detail:os...

asked Oct 17, 2021 in Technique[技术] by 深蓝 (71.8m points)

Categories

Just Browsing Browsing

Most popular tags