How to use arg() function from z3?

Question

I have recently started using z3 API with c++ bindings. My task is to obtain the individual element from an expression

example: (x || !z) && (y || !z) && (!x || !y || z)

How do I get a individual variables by indexing each position using the function arg(i)?

in case of the given example, arg(1) should return the variable 'X'. Is there any other function in z3 that can give me my desired output?

This is the code I tried but the output was not a single variable:

#include<iostream> 
#include<string>
#include "z3++.h"
using namespace z3;

int main()
{
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr z = c.bool_const("z");
    expr prove = (x || !z) && (y || !z) && (!x || !y || z);
    solver s(c);
    expr argument = prove.arg(1);
    std::cout<<argument;  
}

OUTPUT:

(or (not x) (not y) z)(base)

I basically need to make an automated system that indexes every position in the expression and check if its an operator or an operand and insert in into a data structure. So I thought ill create a loop and index every position in the expression. But the arg(i) was not giving me my desired output.

alias alias · Accepted Answer · 2019-06-05T18:43:16

You have to walk through the AST and pick-out the nodes. Z3 AST can be rather hairy, so without knowing exactly what your goal is, it's hard to opine if this is the best approach. But, assuming you really want to walk through the AST, this is how you'd go about it:

#include<iostream>
#include<string>
#include "z3++.h"
using namespace z3;
using namespace std;

void walk(int tab, expr e)
{
    string blanks(tab, ' ');

    if(e.is_const())
    {
        cout << blanks << "ARGUMENT: " << e << endl;
    }
    else
    {
        cout << blanks << "APP: " << e.decl().name() << endl;
        for(int i = 0; i < e.num_args(); i++)
        {
            walk(tab + 5, e.arg(i));
        }
    }
}

int main()
{
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr z = c.bool_const("z");
    expr e = (x || !z) && (y || !z) && (!x || !y || z);

    walk(0, e);
}

When run, this program prints:

APP: and
     APP: and
          APP: or
               ARGUMENT: x
               APP: not
                    ARGUMENT: z
          APP: or
               ARGUMENT: y
               APP: not
                    ARGUMENT: z
     APP: or
          APP: or
               APP: not
                    ARGUMENT: x
               APP: not
                    ARGUMENT: y
          ARGUMENT: z

So, you see exactly where the applications (APP) and arguments (ARGUMENT) are. You can take it from here and construct the data-structure you were talking about.

However, beware that a z3 AST can have many different kind of objects: Quantifiers, numbers, bit-vectors, floats. So, studying the actual AST in detail before you start coding would be a good idea to be aware of all the complexities if you want to make this work for an arbitrary z3 expression.

How to use arg() function from z3?

1 Answers