CODEWITHSUNDEEP
z3z3py
Promise89
Promise89

Reputation: 43

How I run z3 solver on python

Hi I am new on z3 prover, I try to learn this solver but I cant figure out how I run on python. I try to run these codes on python:

    (declare-const A Int)
    (declare-const B Int)
    (declare-const C Int)
    (assert (and
    (= A 98798798987987987987987923423)
    (= B 763429999988888888887364578645)
    (= (+ (* 87 A) (* 93 B)) (+ C C))))
    (check-sat)
    (get-model)

my file name is "ex" and I call "z3 -smt2 ex" but it gives error: ModuleNotFoundError: No module named 'ConfigParser' Also I dont understand how I download z3 tools from this website(https://github.com/Z3Prover/z3/wiki)Thank you!

not: I use Visual Studio Code as a compiler

Upvotes: 0

Views: 1802

Answers (1)

alias
alias

Reputation: 30475

Note that the example you posted is in SMTLib format; i.e., it's not a python program that uses z3py. And z3 -smt2 ex should work just fine on it, since z3 can read SMTLib natively. Since you're getting an error message, your build is most likely busted for some reason. You should follow the download/install instructions in https://github.com/Z3Prover/z3/blob/master/README.md, essentially:

python scripts/mk_make.py -x
cd build
nmake

and report if any of the steps listed there isn't working for you.

Upvotes: 1

Related Questions