CODEWITHSUNDEEP
z3smt
copumpkin
copumpkin

Reputation: 2826

Abstracting over groups of assertions in Z3/SMT-LIB

Are there good mechanisms in Z3 to abstract over assertions? I want to create a “function” that takes in parameters and makes assertions about those parameters, possibly with “local variable” definitions in it.

Imagine that I have a String and I want to assert that it represents a decimal number between 13 and 24. I could write a combination of regular expression assertions about the string and combine it with a str.to.int range assertion. I can do that directly, but if I have dozens of such variables I want to make the assertion about, it gets repetitive. I can use an external language API, or perhaps define a macro/function returning a boolean inside Z3 and assert that it’s true, but that feels a bit indirect. What’s idiomatic here? I want it to be just as easy for Z3 to solve as writing the assertions out by hand

Upvotes: 2

Views: 162

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

You can use define-fun to define a Boolean function f such that you can (assert (f x y z ...)), where f can of course be a conjunction of multiple conditions. The define-fun will be inlined by Z3's SMT2 frontend, i.e., there should not be any runtime cost to it.

(Z3 also supports macros defined via (forall ((x ...)) (= (f x ...) ...)), but you need to explicitly apply the model-finder tactic to inline them.)

Upvotes: 2

Related Questions