CODEWITHSUNDEEP
z3smt
JRR
JRR

Reputation: 6152

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?

Upvotes: 1

Views: 190

Answers (1)

alias
alias

Reputation: 30525

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!

Upvotes: 0

Related Questions