z3 — отсутствующие методы модификации в API C ++

Question

z3 — отсутствующие методы модификации в API C ++

Я хотел сделать некоторые преобразования для объекта z3 :: expr. Как я могу использовать Z3_substitute_vars, Z3_translate а также Z3_substitute_ с C ++ API? Они реализованы в C #, но я не могу найти их в C ++. Очень странно, что они не реализованы.

Я пытался использовать C api, но безрезультатно, вот пример:

void substitute(){
z3::context c;
z3::expr a = c.int_const("a");
Z3_ast astA = a;
z3::expr plus = 2*a;
errs() << Z3_ast_to_string(c,plus);
z3::expr b = c.int_const("b");
Z3_ast astB = a;
z3::expr subs(c,Z3_substitute(c,plus,1,&astA,&astB));
errs() << Z3_ast_to_string(c,subs);
}

Но a не подставляется. Я делаю что-то неправильно?

0

c++z3

Решение

Другие решения

Я считаю, что ваш пример имеет опечатку:

  Z3_ast astB = a;

Пытаться

  Z3_ast astB = b;

1

Источник

Accepted Answer

Спасибо за указание на то, что эти функции отсутствуют.
Оболочка C ++ добавляет удобства помимо C API, и это
будет разумно добавить удобства для этих функций API
а также, поскольку вы указываете, что используете их.

Оболочки C ++ все еще могут использоваться вместе с базовым C API.
Поэтому вы можете вызывать функции, такие как Z3_translate и Z3_substitute
при использовании C ++ API. Ряд других функций API также не
присутствует в оболочке C ++, но способ, которым обернуты существующие функции
должен дать очень хорошее представление о том, как вызывать остальные функции.

Вот несколько похожих постов:

2