CODEWITHSUNDEEP
c++z3smt
GermanShepherd
GermanShepherd

Reputation: 151

How does Z3 convert expr to SMT?

While trying to learn about the Z3 tool, I am puzzled by how Z3 construts expressions. Also, I'm new to this, I have gone through related, questions, and they do not answer my query.

Using Z3, (say cpp implementation) , suppose there is an expression

expr e1=((x[0]=tru && y[0]!=tru)||(x[0]!=tru &&y[0]=tru));

Where tru is a tautology.

on printing this expression, the tool displays the following tree:

 (let ((a!1 (and (or x0 (not x0)) (distinct y0 (or x0 (not x0))))))
      (or a!1 (or x0 (not x0))))

and this is not what I wanted my e1 to represent. This seems to be an efficient/pretty/shorthand of what I have written.

Firstly, Can I somehow, convert expr to SMT myself, so that I can check if it is being translated correctly?

Secondly, is there a way to print the expression in the simple way I represented it, and not in an efficient structure(using subtrees, like a!1 and so on) in SMT language? Perhaps a switch that I can turn off? This probably requires indepth knowledge of the tool, hence I have tagged this question accordingly.

Upvotes: 0

Views: 186

Answers (1)

alias
alias

Reputation: 30418

Some of the "translation" is unavoidable. As Z3 constructs the parse-tree for your expressions, it will rewrite them to internal forms. This isn't merely for "efficiency." It is also the case that some surface forms just don't have an internal representation, but is rather rewritten.

Pretty-printing is another matter, of course. There are many ways to control how pretty printing is done. If you run z3 -p and look at the output for the pretty-printing section, you see:

[module] pp, description: pretty printer
    bounded (bool) (default: false)
    bv_literals (bool) (default: true)
    bv_neg (bool) (default: false)
    decimal (bool) (default: false)
    decimal_precision (unsigned int) (default: 10)
    fixed_indent (bool) (default: false)
    flat_assoc (bool) (default: true)
    fp_real_literals (bool) (default: false)
    max_depth (unsigned int) (default: 5)
    max_indent (unsigned int) (default: 4294967295)
    max_num_lines (unsigned int) (default: 4294967295)
    max_ribbon (unsigned int) (default: 80)
    max_width (unsigned int) (default: 80)
    min_alias_size (unsigned int) (default: 10)
    pretty_proof (bool) (default: false)
    simplify_implies (bool) (default: true)
    single_line (bool) (default: false)

You can play around with these settings to control how the pretty-printing is done, which might fit your needs better. In particular, from your problem description, I recommend setting the following two parameters:

    pp.max_depth      --> 4294967295
    pp.min_alias_size --> 4294967295

(The number doesn't really matter, just make them large enough.) These two settings should avoid the pretty-printer from creating the a!1 subtrees, you are seeing.

Unfortunately what these options exactly mean isn't all that well documented. Some of them, you can guess from their name, others you can play around and see what their impact is. But if you really want to know how they change the output, you'll have to dig into the z3 source code itself. Best of luck!

Upvotes: 1

Related Questions