Сохранение параметров функции implies () в z3 - PullRequest
Новая
       11

Сохранение параметров функции implies () в z3

0 голосов
/ 07 июня 2019

Я хочу создать функцию, которая может хранить левый и правый параметры функции implies () в 2 различных переменных выражения.Решение с кодом очень заметно.Спасибо.

Это то, что я пробовал раньше.

#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 = implies(z,(x && y));
    walk(0, e);
}

и это был вывод: 

APP: =>
     ARGUMENT: z
     APP: and
          ARGUMENT: x
          ARGUMENT: y

1 Ответ

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

Я просто сделаю свой комментарий явным с помощью примера: 

if (e.is_implies()) {
    cout << "left side: " <<endl;
    walk(4, e.arg(0));
    cout << "right side: " <<endl;
    walk(4, e.arg(1));
}

При этом используются методы is_implies и arg класса expr. Документация

...