As a convenience to the C programmer, Z3 has some pre-written C/C++ for commonly-met-with algebraic datatypes. ADTs are polynomial type constructors: x×y×z+….
"Tuples" are monomial (i.e. 1-injection) datatypes. "Enumerations" are 0-degree polynomials. "List" provides convenience C code for the standard "nil+cons" construction.
This commit also implements related Z3CAPITests which previously either lived in Z3CAPITODOTest or were missing altogether.
As a convenience to the C programmer, Z3 has some pre-written C/C++ for commonly-met-with algebraic datatypes. ADTs are polynomial type constructors: x×y×z+…. "Tuples" are monomial (i.e. 1-injection) datatypes. "Enumerations" are 0-degree polynomials. "List" provides convenience C code for the standard "nil+cons" construction.
This commit also implements related Z3CAPITests which previously either lived in Z3CAPITODOTest or were missing altogether.