Is there any templating engine for smtlib2 (alternatively z3)?

Question

I was wondering if there are is any way to represent an smtlib2 formula as a template. For instance:

(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))))

can be represented as (say using jinja2-style templating)

((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}}))))

And then the template can be rendered to represent an actual smtlib formula:

(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))))

Is there any natural way to do this other than use something like jinja2 and create my own template for every formula?

Alternatively, considering that I already have a z3::expr_vector that represents an SMT formula, is there a way to "templatize" it? My eventual goal is that I would like to "invoke" the templatized version with unique bitvector names for each invocation. Does the z3 C++ API have any methods which naturally allows one to achieve this?

Answer 1

There isn't anything in the z3 C++/Java API's to do this. However, if you're programming in C++ or Java, simply write a function that produces this expression. You're saying that you already have a z3::expr_vector; you should instead write a function that takes the relevant parts (i.e., variable names and sizes), and then constructs this final expression; i.e., regular programming using the z3 AST.