Skip to content

API change: convert the abstract class "FormulaType" to interface.#615

Open
kfriedberger wants to merge 2 commits intomasterfrom
formulatype-to-interface
Open

API change: convert the abstract class "FormulaType" to interface.#615
kfriedberger wants to merge 2 commits intomasterfrom
formulatype-to-interface

Conversation

@kfriedberger
Copy link
Member

The idea for this change was brought up in a comment about potential API changes.

This change makes JavaSMT more open for user applications, as it allows them to define their own formula types and use them in JavaSMT. This also blocks us from marking this class as "sealed" at some time in the future, because users can inherit from it.

We can discuss benefit and/or negative effects from this change.

This change makes JavaSMT more open,
and allows user applications to define their own formula types and use them in JavaSMT.
This also blocks us from marking this class as "sealed" at some time in the future,
because users can inherit from it.
@ThomasHaas
Copy link
Contributor

Just to extend the discussion from #611 a bit.

Inheriting from the JavaSMT types is generally dangerous in that the user-specified types will not interact well (if at all) with the existing methods in JavaSMT. Essentially, a custom type cannot be used as a parameter to any method of JavaSMT.
However, the user can put simple wrappers around JavaSMTs interface to handle the custom types in several cases. To give a concrete example, I refer to Dartagnan's custom TupleFormula/TupleFormulaManager and the necessary wrappers FormulaManagerExt for extending ITE to custom tuples, and ModelExt for extending model evaluation to tuples.

In a similar way, record types could be implemented on the user-side, or more specialized types like PointerFormula (consisting of, e.g., EnumerationFormula object and an IntegerFormula address).

I have not tested how far the user could go with custom wrappers. IIRC, the fact that FormulaType was effectively sealed was a problem though.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants