Search code examples
z3smt

is there a way to include another file in smtlib?


Similar to #include in C in importing functions and axioms that are defined in another file. I wasn't able to find such functionality described in the SMTLIB documentation or from the online examples. Any hints?


Solution

  • SMTLib has no means of #include'ing or importing other files. This might look like a shortcoming, but it is quite rare for people to hand-write SMTLib files: It is almost always machine generated from a higher level language, and it is assumed that whoever generates the SMTLib can simply spit out one big file that includes everything you need.

    Having said that, I think this would be a useful feature to have indeed. SMTLib standard is always evolving and such features are usually discussed in their mailing list:

    https://groups.google.com/forum/#!forum/smt-lib

    Feel free to join the discussion and make a request!