BitVectors (which contain their scope in the sort) within the ScopeMap?

WatForm / fortress

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

MIT License

5 stars 0 forks source link

Open nancyday opened 2 months ago

nancyday commented 2 months ago

BitVector(n) MUST be mapped to a scope of 2^n (should be checked somewhere)
should these be of fixed scope? (IntToBVTransformer does not currently make them fixed)
how should it be handled in any transformer that considers the scopes (QuantifierExpansion, TransitiveClosure, MaxUnboundedScopes, etc)