Как использовать метод «bit-blast» для печати заданной формулы в логической форме высказываний? - PullRequest
Новая
       9

Как использовать метод «bit-blast» для печати заданной формулы в логической форме высказываний?

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

Я создаю функцию, которая преобразует формулу битового вектора в логическую форму предложения. Тактика, называемая «бит-взрыв», обрабатывает такие выражения бит-вектор в форме PL.

Я пытался создать программу, которая принимает выражения битовых векторов и применяет к ним тактику битового взрыва. Но так как я новичок в этой теме, я не могу понять, как распечатать вывод после дробеструйного выражения. 

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

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 16);
    expr y = c.bv_const("y", 16);
    expr z = c.bv_const("z", 16);
    goal g(c);
    g.add(z == x + y);
    std::cout<<g;


}

Это код, который я пробовал, но он не принимает выражение "z = x + y" Но процесс, который я делаю, правильный? Если нет, то как я должен распечатать выражение после применения к нему бит-бласта ??1006*

Спасибо.

1 Ответ

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

Используйте ==, а не =. То есть z == x + y. И тогда вам, конечно, придется применить тактику: 

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

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 16);
    expr y = c.bv_const("y", 16);
    expr z = c.bv_const("z", 16);
    goal g(c);
    g.add(z == x + y);
    apply_result r = t(g);
    std::cout << r << endl;
    return 0;
}

Это печатает убитую битой цель; это довольно долго, поэтому я не буду здесь это вставлять.

Если вы хотите извлечь фактическое выражение, вам нужно немного больше программировать. (Между прочим: вам действительно нужно сначала изучить API https://z3prover.github.io/api/html/z3_09_09_8h_source.html.)

Вот пример (я меняю исходное выражение, чтобы вывод был достаточно маленьким, чтобы его можно было понять.): 

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

int main()
{   context c;
    tactic t = tactic(c, "bit-blast");
    expr x = c.bv_const("x", 2);
    expr y = c.bv_const("y", 2);
    goal g(c);
    g.add(y == ~x);
    apply_result r = t(g);
    if(r.size() > 0)
    {
       expr res = r[0].as_expr();
       cout << res << endl;
    }
    else
    {
        cout << "tactic failed" << endl;
    }
    return 0;
}

Это печатает: 

$ c++ a.cpp -lz3; ./a.out
(and (not (= k!0 k!2)) (not (= k!1 k!3)))

И да, вы получите k!0 и т. Д. В качестве индексов, которые вам будет довольно сложно соотнести с вашими x и y; но это неизбежно: бит-бластер представит новые переменные, а в API есть все кусочки, чтобы восстановить то, что вам нужно: https://z3prover.github.io/api/html/z3_09_09_8h_source.html

...