Unique name generation for transitive closure

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic

MIT License

5 stars 0 forks source link

Open otzzila opened 3 months ago

otzzila commented 3 months ago

The transitive closure operations introduce new function declarations, but do not ensure their new names are unique.

For example ClosureEliminatorEijck defines val closenessName: String = "^Close^" + functionName;.

We should use the NameGenerator to ensure added functions use unique names in these operations.