Hi: While it is true that reordering the Expr constructions
can improve the speed, the key problem here unfortunately is
that Alloy type checker requires us to coalesce the type into a minimum.

Short story:

  // this following model will take a *long* time to type check:
  abstract sig Base { }
  one sig A, B, C, D, E, F, ..., Z extends Base { }
  fact { some A->A + A->B + ... A->Z + B->A + B->B + .. + Z->Z }

  // the following model is amazingly fast to typecheck
  abstract sig Base { }
  one sig A, B, C, D, E, F, ..., Z extends Base { }
  fun promote:Base->Base { none->none }
  fact { some promote + A->A + A->B + ... A->Z + B->A + B->B + .. + Z->Z }

Now, the long story:

Model 1:
Type of A->A is A->A
When adding A->B to it, the typechecker checks if A->B can be subsumed by A->A.
It cannot. So the combined expression (A->A+A->B) has type (A->A+A->B).
When adding A->C to it, the typechecker checks if A->C can be subsumed by A->A or A->B.
It cannot... etc. etc. Each additional term triggers a type hierarchy comparison
against all previous terms, with a total of 228826 type-subset-checks!

Model 2:
The type of promote is Base->Base.
When adding A->A to it, the typechecker sees A->A can be subsumed by Base->Base.
So the combined expression (promote+A->A) has type Base->Base.
Likewise for adding A->B, and A->C, and...
So this time, the final expression's type is exactly Base->Base,
and only 676 type-subset-checks were performed in the process.

The reason why the typechecker carefully merges types is to
try to have as-precise-as-possible type information
in order to resolve ambiguous names. That's the main purpose.
However, API users have no such need for disambiguation.

Basically it's a trade-off: precise type info is expensive to compute.

So if you don't think you need the most-precise-type for disambiguation,
then you should use some trick to deliberately broaden up the type.

For Alloy Analyzer users, writing a function that returns none->none but has type univ->univ
would flatten the type maximally.

For Alloy API users, writing the expression UNIV.product(UNIV).minus(UNIV.product(UNIV))
would flatten the type maximally, since the typechecker would assume (univ->univ - anything) is still
of type univ->univ.

Sorry my answer is a bit long, but basically if you're already trying to contort
your Expr construction routines, then you might as well just flatten its type using
a magical expression (which you can construct once, and then reuse over and over again).
And this would alleviate the need for complicated re-ordering.  Just always start
with an Expr whose type is maximally flat (ie. univ, or univ->univ, or univ->univ->univ).

Sincerely,
Felix Chang

Thanks Felix, this seems to work a *lot* faster for constructing a problem;
however, I think that there is a caveat to this trick.

Roughly, I construct a problem like this:

abstract sig A {}
abstract sig B { a:A }

one A1,A2,A3 extends A {}
one B1,B2,B3 extends B {}

fun promote:B->A{ none->none }
fact { a = promote + B1->A1 + B1->A2 + B2->A2 + B3->A3 }

Since this is done using the API, I did as you suggested, i.e.:

Field a = ...
Expr constraint = Sig.UNIV.product(Sig.UNIV).minus(Sig.UNIV.product(Sig.UNIV));
while (Expr tuple : tuples) { constraint = constraint.plus(tuple); }
Expr bound = a.equal(constraint);

When I try to compute a solution, I get an error in edu.mit.csail.sdg.alloy4compiler.translator.A4Solution:

TupleSet query(boolean findUpper, Expression expr, boolean makeMutable) throws ErrorFatal {
  ...
  throw new ErrorFatal("Unknown expression encountered during bounds computation: "+expr);
}

This code doesn't know how to handle binary expressions with a difference operator.
If I run this on a large problem, expr can have hundreds or thousands of tuples which brings another problem:
The ErrorFatal constructor induces tons of calls to:

StringBuilder.append(Object)
BinaryExpression.toString()
String.valueOf(Object)

This blows up the stack...

Is the promotion trick really kosher for expression bounds?

Nicolas Rouquette
Flight Software Engineering & Architecture Group
Jet Propulsion Laboratory, Caltech, Pasadena, CA, USA

>
> When I try to compute a solution, I get an error in edu.mit.csail.sdg.alloy4compiler.translator.A4Solution:
>

Hi:  That's a bug in Alloy4's API interface, though Alloy4 GUI users probably won't ever trigger it.
I'll try to see if I can reproduce the bug from your description above; if I cannot, then I'll need you to try to
send me a small file that triggers it.

>
> If I run this on a large problem, expr can have hundreds or thousands of tuples which brings another problem:
>

The exception object should only be built when there is a user error or a tool error (such as the Alloy4 bug above).
So once I fix the Alloy4 bug, then this second point goes away as well.

Sincerely,
Felix Chang

In the meantime, I turned off the promotion trick and used the logarithmic technique for constructing expression bounds.
I'm running into problems elsewhere:

BoundsComputer(A4Reporter, A4Solution, ScopeComputer, Iterable)
calls A4Reporter.bound(String) with a potentially expensive message to construct:

Expression sim = sim(f.decl().expr);
                 if (sim!=null) {
                    rep.bound("Field "+s.label+"."+f.label+" defined to be "+sim+"\n");
                    sol.addField(f, sol.a2k(s).product(sim));
                    continue;
                 }

Because 'sim' is a very large expression, printing it can blow up the stack.

Once I manage to compute the CNF for this problem, I can run the profiler to see where the bottlenecks are.
Without the CNF, it's hard to give you a reproducible test case because all of this construction is happening using a reflective EMF => Alloy mapping.

Nicolas Rouquette
Flight Software Engineering & Architecture Group
Jet Propulsion Laboratory, Caltech, Pasadena, CA, USA

Note that A4Solution.query(boolean, Expression expr, boolean) throws exceptions that can be very expensive to construct if ex[r is a complex expression:

       throw new ErrorFatal("Unknown expression encountered during bounds computation: "+expr);

For expression bounds of the form:

b = tuple + tuple + ....

these exceptions are ignored in Simplifier.simplify_equal(Expression, Expression)

This suggest replacing the argument of the ErrorFatal() constructor above with something cheap even if expr is very complicated.

Nicolas Rouquette
Flight Software Engineering & Architecture Group
Jet Propulsion Laboratory, Caltech, Pasadena, CA, USA

>
> A4Solution.query(boolean, Expression expr, boolean)
> throws exceptions that can be very expensive to construct
> if expr is a complex expression
>

Yes I know the exception object can take a lot of resources to construct
when the Expr involved is complicated.

The question is, given that the exception is only constructed
when there is an actual error (either the user's fault or my fault),
then the fact that the error reporting itself ran out of memory/time is not
something we need to work hard on.

(It's hard because you can't figure out if an error message will be long or
not unless you do a tree walk on the Expr node... so to do that, we'll have
to watch out for stackoverflow, and have a mechanism to stop the message half
way thru the recursion... etc. etc. All these additional hundreds of lines
of code (since it has to be done for every Expr type) adds more chances of
bugs, and long term maintenance headache)

>
> rep.bound("Field "+s.label+"."+f.label+" defined to be "+sim+"\n");
>

Hmm, that's a interesting issue. Hmm, it's a hard problem to deal with
using the current REPORTER pattern (where the Alloy4 API doesn't know whether
a reporter cares about a particular message, so Alloy4 API dutifully
construct full messages for everything the reporter may care about,
but the reporter (in your case I hope) will just throw this message away.

Okay, how about if I change the reporter method to return a boolean.
So Alloy4 API will always first call the reporter with "" (which the reporter
should then always ignore), and if the reporter returns true (meaning he cares),
then Alloy4 API will construct a detailed message for that reporter method.

What do you think of this idea?

(By the way, you've identified two direct issues and one quality-of-implementation issue.
We can probably work them out via direct emails, then I can post the final resolution to this thread)

Sincerely,
Felix Chang