A TupleFormula is basically a List<Formula>, a special type of ADT. Such a formula is helpful to encode structs or custom types like pointers (e.g, as (base, offset) or generally (provenance, address) tuples). Note that tuples can be nested, but they cannot be properly recursive.
A TupleFormulaManager would provide at least extract, insert, construct, and equality methods.
These can be implemented generically over all backend SMT solvers in a very lightweight manner (see Dartagnan's TupleFormula and TupleFormulaManager for reference).
Unlike other formula managers, the method makeVariable does not need to be provided as the user can easily simulate it, e.g.,
makeVariable(<int, int> var) ~ construct(makeVariable(int var#1), makeVariable(int var#2)).
Technically JavaSMT could also do this trick internally, but then it would create internal variables in a non-transparent way to the user and it would also need to maintain a mapping between tuple variable names and the internally-generated variable names, which is ugly IMO.
Several SMT solvers like Z3, Yices2, and CVC5 natively support tuples and so a generic implementation might not be necessary at all!
Problems:
- There are infinitely many possible
TupleFormulaTypes and so they cannot be possibly captured by the Java type system in a totally type-safe manner. This means that insert would take a generic Formula<?> to insert and do a runtime check to see if it matches the type of the tuple (insert should not silently change the type of tuples!).
extract is a little bit more annoying on the user side as (i) JavaSMT does not know what to type the user expecting to get (no runtime check possible) and (ii) the user needs to cast the returned formula to its proper type to make it really usable. JavaSMT could provide an overload
<T extends Formula> extract(TupleFormula f, int index, FormulaType<T> expectedType) that takes an expected formula type as input to do both runtime checks and automatic casting.
- The generic implementation likely interacts badly with other parts of the API like dumping & parsing, or
FormulaVisitors. This might be a strong argument against implementing it inside JavaSMT.
Alternative: A RecordFormula with named members might also be interesting (Map<String, Formula> instead of List<Formula>). Technically, records can simulate tuples. I think some SMT solvers also support them.
This is a mere suggestion and not necessarily a feature request as our custom solution in Dartagnan works reasonable well at the moment.
A
TupleFormulais basically aList<Formula>, a special type of ADT. Such a formula is helpful to encode structs or custom types like pointers (e.g, as(base, offset)or generally(provenance, address)tuples). Note that tuples can be nested, but they cannot be properly recursive.A
TupleFormulaManagerwould provide at leastextract,insert,construct, andequalitymethods.These can be implemented generically over all backend SMT solvers in a very lightweight manner (see Dartagnan's TupleFormula and TupleFormulaManager for reference).
Unlike other formula managers, the method
makeVariabledoes not need to be provided as the user can easily simulate it, e.g.,makeVariable(<int, int> var) ~ construct(makeVariable(int var#1), makeVariable(int var#2)).Technically
JavaSMTcould also do this trick internally, but then it would create internal variables in a non-transparent way to the user and it would also need to maintain a mapping between tuple variable names and the internally-generated variable names, which is ugly IMO.Several SMT solvers like Z3, Yices2, and CVC5 natively support tuples and so a generic implementation might not be necessary at all!
Problems:
TupleFormulaTypesand so they cannot be possibly captured by the Java type system in a totally type-safe manner. This means thatinsertwould take a genericFormula<?>to insert and do a runtime check to see if it matches the type of the tuple (insertshould not silently change the type of tuples!).extractis a little bit more annoying on the user side as (i) JavaSMT does not know what to type the user expecting to get (no runtime check possible) and (ii) the user needs to cast the returned formula to its proper type to make it really usable.JavaSMTcould provide an overload<T extends Formula> extract(TupleFormula f, int index, FormulaType<T> expectedType)that takes an expected formula type as input to do both runtime checks and automatic casting.FormulaVisitors. This might be a strong argument against implementing it inside JavaSMT.Alternative: A
RecordFormulawith named members might also be interesting (Map<String, Formula>instead ofList<Formula>). Technically, records can simulate tuples. I think some SMT solvers also support them.This is a mere suggestion and not necessarily a feature request as our custom solution in Dartagnan works reasonable well at the moment.