Open nancyday opened 1 month ago
It looks like for each sort S, DEsToConstantsTransformer
generates all DE constants from 1 to scope(S)
regardless of whether they're used. I assume this is why it doesn't generate DEs for unbounded sorts.
Unless they're needed to assert an exact scope for the sort (or a lower bound in the case of unbounded sorts), I don't think it should be necessary to generate constants for DEs that don't appear in the problem (including quantifier expansion, etc). This would solve this problem as well as give a performance boost in the case that some DEs don't appear. This would not require the scope of the sort with DEs to be fixed. CC @otzzila
I think we are required to generate constants for all domain elements (whether they are in the problem or not) to guarantee a finite problem. All domain elements would be used in quantifier expansion for a finite sort anyway.
When are DEs used in the original theory when they are not of a fixed scope sort (such as an enum from a one sig)? Integer DEs may be a special case here.
Portus generates DEs in these cases: one sigs, the ordering module, and expanding over sums. Of these, Portus marks a sig which is expanded over for sum as fixed; Portus does not currently mark ordered sigs as fixed, but I think it should because the size is assumed when defining next
(and indeed Alloy even forces an ordered sig to be exact) - I'll push a commit to fix this in a moment.
This leaves one sigs. I think it's possible to sensibly have a one sig without marking its containing sort as fixed. For example:
sig State {}
one sig InitialState extends State {}
This is an example of a non-enum use of one sigs: here the one sig is effectively used to pick a single arbitrary element of State
. It still makes sense to change State
's scope in the Portus output as long as it has at least one element so that InitialState
can have a value (in general: if a sig has k one sigs, its scope must be at least k for the model to make sense, although maybe it would be acceptable for it to just be unsat in that case).
So for unbound sorts for which domain elements are used in the model, I think it makes sense to just generate constants for the domain elements that are used in the model. In the above example, that would correspond to generating one constant for InitialState
, which would force the interpretation of State
to have size at least 1.
Thinking about the ordering module more, taking this example:
open util/ordering[A]
sig A {}
run {} for 4 A // Alloy forces this to be 'exactly 4 A'
We don't actually rely on the size of the sort of A, per se. Instead, we assign A a range of domain elements within its sort and define first
and next
based on those domain elements. If there were other sigs in A's sort, so that the size of A is specified via axioms, then we could make A's sort unbound without problems.
However, since A is the only sig in its sort, its membership predicate is optimized away and A will have the same size as its containing sort, meaning that it's semantically incorrect to change A's sort since the ordering module relies on A having an exact scope known ahead of time.
I think this is a special case of a more general problem: whenever a sig is exact and takes up the whole sort, making it unbound removes the exactness. In the general case, we don't know whether it's semantically correct in any particular model to change the value of an exact scope (in the ordering case it's not, and for example maybe a model author relies on a sig having a scope of exactly some value for a domain-specific reason).
So perhaps every sig that has an exact scope and takes up its entire sort (and the membership predicate optimization is active) should have its sort marked fixed?
I've been trying to follow the previous example here. Isn't sort A going to be of fixed size because of the ordering module?
Is there some connection between a subset of a sort being exact and that forcing the requirement that the sort's scope is exact?
For the earlier example, I think your point is that the creation of one sigs creates a lower bound on the number of elements in the sort but not an upper bound. Meaning the scope does not have to be exact or fixed but has to be above the number of distinct values of the one sig?
[Long comment as I try to work out options here]
I think portus is using DEs as values of the domain that are distinct
.
There seem to be two cases for Portus: i) a sort that has some distinct values but the scope of the sort is not limited to those distinct values ii) a sort that has a fixed set of distinct values - this is the role of an enum. EnumsToDEs replaces the enums with DEs and sets the sort to have a fixed size.
I believe that currently Portus does
Side question: How do the DEs used in the theory relate to the DEs created for the sort? Are they guaranteed to be the first DEs used for the sort in its finite enumeration by Fortress? or by Portus? I couldn't understand the answer to this question from the DomainElement constructor in Term.scala . @jporemba ? @ryandancy ?
In the options below, I'm trying to think whether there is a difference between a) min scope=x, max_scope!=infinity because the sort has x distinct DEs for sure but could have more if min_scope != max_scope and b) min scope!=max_scope!= infinity because the scope is non-exact. (min_scope cannot be infinity?)
If we have an unbound sort (max_scope=infinity), we don't expand over the elements of the domain in quantifier expansion or range formulas.
I see a few options here:
for one sigs, portus creates constants (not DEs) plus the axiom that these constants are distinct (let's call this the theory's distinctness axiom).
Fortress scans a theory for DEs used in the input theory. It collects that ones in use and creates an axiom that those are distinct. This effectively does option 1 internally to Fortress and has the same disadvantage of 1.
We adjust scopes for allow for a minimum scope (as well as our current maximum scope) as kodkod does.
I'm not certain about what the eliminating NonExactScopesTransformer (not currently in use by portus) with predicates would do. Perhaps it could just assert that the membership predicate is true of DEs up to the minimum scope as well as what it currently does (adding predicates as guards to expression).
Eliminating NonExactScopes with non-distinct constants (a method @jporemba tried, but I don't think is left in the code base - although perhaps there is no NonExactScope eliminator transformer in that version) works nicely with option 3. For non-exact scope, Joe tried of allowing constants representing DEs to be non-distinct. There is a version of DEsToConstants that will not generate the constant's are distinct axiom. With a minimum scope, that option would have to be redone to generate a distinctness axiom for the minimum scope elements.
I'm also not certain what the DEsToDatatypesTransformer should do. It asserts that there are x distinct elements of a sort via a datatype declaration in SMT-LIB. (It actually turns the finite scope limit into an enum, which is written to SMT-LIB as a datatype declaration.) It doesn't seem to make sense to use this with anything other than an exact scope.
I will continue to think about whether there are any other possible effects of moving to a min/max scope scheme.
I agree with the characterization of how DEs are used in Portus in the first part of your comment. Portus does not currently use enums at all, although you make a good point that some uses of DEs are effectively equivalent to enums and could be translated as such.
This is probably actually a Portus issue although discussion here may be relevant. The bug appears because constants are unknown in the write to SMT-LIB during solving. These constants have come from DEs in sorts that became unbounded. I think that constants were never introduced in the theory because no constants are introduced for an unbounded sort.
For example,
If we look at the 4-bit adder in Alloy, this line: one sig A, B, C, S extends BitVector { } would make BitVector an enum? with A,B,C,S as enum values? Would that make BitVector of fixed scope?
Fundamentally, should the use of DEs in building terms at the API require the scope of the sort to be fixed? Is there any use case where it is not bound?