Как использовать функцию arg () из z3? - PullRequest
Новая
       18

Как использовать функцию arg () из z3?

2 голосов
/ 05 июня 2019

Я недавно начал использовать z3 API с привязками c ++.Моя задача - получить отдельный элемент из выражения

пример: (x || !z) && (y || !z) && (!x || !y || z)

Как получить отдельные переменные путем индексации каждой позиции с помощью функции arg (i)?

в случае данного примера arg (1) должна возвращать переменную 'X'.Есть ли в z3 какая-либо другая функция, которая может дать мне желаемый результат?

Это код, который я пробовал, но вывод не был единственной переменной: 

#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;  
}

ВЫХОД: 

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

Мне в основном нужно сделать автоматизированную систему, котораяиндексирует каждую позицию в выражении и проверяет, является ли он оператором или операндом, и вставляется в структуру данных.Поэтому я подумал, что не буду создавать цикл и индексировать каждую позицию в выражении.Но arg (i) не давал мне желаемого результата.

1 Ответ

1 голос
/ 05 июня 2019

Вы должны пройти через AST и выбрать узлы. Z3 AST может быть довольно волосатым, поэтому, не зная точно, какова ваша цель, трудно определить, является ли это лучшим подходом. Но, если вы действительно хотите пройти через AST, вот как вы это сделаете: 

#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);
}

При запуске эта программа печатает: 

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

Итак, вы точно видите, где находятся приложения (APP) и аргументы (ARGUMENT). Вы можете взять его отсюда и построить структуру данных, о которой вы говорили.

Однако имейте в виду, что в z3 AST может быть много разных типов объектов: квантификаторы, числа, битовые векторы, числа с плавающей запятой. Итак, детальное изучение фактического AST перед началом кодирования было бы хорошей идеей, чтобы знать обо всех сложностях, если вы хотите выполнить эту работу для произвольного выражения z3.

...