Есть ли механизм шаблонов для smtlib2 (или z3)?

Question

Мне было интересно, есть ли способ представить формулу smtlib2 в качестве шаблона. Например:

      (declare-fun b () (_ BitVec 16))
(declare-fun a () (_ BitVec 8))
(declare-fun c () (_ BitVec 32))
(assert (= c (bvor ((_ zero_extend 24) a) ((_ zero_extend 16) b))))

может быть представлено как (скажем, с использованием шаблонов в стиле jinja2)

      ((declare-fun {{B_VAR}} () (_ BitVec {{B_VAR_SIZE}}))
(declare-fun {{A_VAR}} () (_ BitVec {{A_VAR_SIZE}}))
(declare-fun {{C_VAR}} () (_ BitVec {{C_VAR_SIZE}}))
(assert (= {{C_VAR}} (bvor ((_ zero_extend 24) {{A_VAR}}) ((_ zero_extend {{B_VAR_SIZE}}) {{B_VAR}}))))

Затем шаблон можно отобразить для представления фактической формулы smtlib:

      (declare-fun P () (_ BitVec 16))
(declare-fun Q () (_ BitVec 8))
(declare-fun R () (_ BitVec 32))
(assert (= R (bvor ((_ zero_extend 24) Q) ((_ zero_extend 16) P))))

Есть ли какой-нибудь естественный способ сделать это, кроме как использовать что-то вроде jinja2 и создать свой собственный шаблон для каждой формулы?

В качестве альтернативы, учитывая, что у меня уже есть z3::expr_vector, который представляет формулу SMT, есть ли способ «шаблонизировать» ее? Моя конечная цель состоит в том, что я хотел бы «вызывать» шаблонную версию с уникальными именами битовых векторов для каждого вызова. Есть ли в z3 C++ API какие-либо методы, которые естественным образом позволяют добиться этого?

Answer 1

В z3 C++/Java API нет ничего для этого. Однако, если вы программируете на C++ или Java, просто напишите функцию, которая производит это выражение. Вы говорите, что у вас уже есть z3::expr_vector; вместо этого вы должны написать функцию, которая берет соответствующие части (т. е. имена и размеры переменных), а затем строит это окончательное выражение; т.е. обычное программирование с использованием z3 AST.