I am trying to use the Z3 solver (which works over SMT-LIB) to reason over C programs involving structs. I would like some way to represent that the struct is a variable that contains other variables in SMT-LIB, but I can't find a way to do that. Does anyone know of a way to represent C structs in SMT-LIB?
1 Answers
1
votes
You can use algebraic data types feature of SMTLib 2.6 to model structs. See Section 4.2.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
This feature allows not only regular struct declarations but also recursive ones; i.e., you can also model structs that have fields of the same type.
I should add that algebraic data types in SMT are actually more general than what you need, they actually can be used to model values constructed with different algebraic constructors. (For the straightforward record case, you'll simply use one constructor.)
Algebraic-data types are rather a new feature in SMTLib, but both Z3 and CVC4 support it. Solver quality might vary depending on the features you use, but if you simply use datatypes to construct and deconstruct values it should work pretty much out of the box.
