search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.4k stars 1.47k forks source link

Z3 prints n-ary concats but SMT-LIBv2 only supports 2-ary concats #2285

Closed dbueno closed 5 years ago

dbueno commented 5 years ago

I am using z3 to print some formulas from the python api using formula.sexpr(). I'm on the master branch of Z3, commit 6e3f05b98. After printing the formula with z3, I'm parsing it with mathsat, which errors out.

Z3 prints (concat ...) as an n-ary application. Mathsat only parses binary applications. It appears from my reading of the smt-lib2 BV standard (http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml) that only binary applications of concat are allowed, so it seems like z3 should print binary applications for smt-lib2 compliance.

Is there any way to get Z3 to print binary applications of concat only?

I've tried the options:

set_param("pp.flat_assoc", False) set_param("rewriter.flat", False)

to no avail.

I also tried:

set_param("smtlib2_compliant", True)

and this also didn't fix the concats.

It looks like the concat's are being introduced during calls to simplify() on zero-extension operations, if that helps. I'm working on a standalone test case.

NikolajBjorner commented 5 years ago

Z3 uses n-ary concats internally and it is convenient to round-trip this convention as it is an AC operation. You can write a script that converts n-ary concats to binary form for interfacing with MathSAT.