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?
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!