Cast exception in some programs

[pkriens]

The following program:

run {
    minsome Int
}

Created the following exception:

Executing "Run run$1"
   Sig this/Univ scope <= 3
   Sig this/Univ in [[Univ$0], [Univ$1], [Univ$2]]
   Generating facts...
   Simplifying the bounds...
   Solver=sat4jmax Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20
   Generating CNF...
   Generating the solution...
.(see the .)
Unknown exception occurred: java.lang.ClassCastException:
kodkod.engine.bool.BooleanConstant cannot be cast to
kodkod.engine.bool.BooleanFormula

The same exception occurred in a larger program that did not use Int as the optimization target, which I can understand is special as usual.

Stack trace:

class edu.mit.csail.sdg.alloy4.ErrorFatal: Unknown exception occurred: java.lang.ClassCastException: kodkod.engine.bool.BooleanConstant cannot be cast to kodkod.engine.bool.BooleanFormula
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:587)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:684)
edu.mit.csail.sdg.alloy4.WorkerEngine$5.run(WorkerEngine.java:468)
java.base/java.lang.Thread.run(Unknown Source)
caused by...
class java.lang.ClassCastException: kodkod.engine.bool.BooleanConstant cannot be cast to kodkod.engine.bool.BooleanFormula
kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:939)
kodkod.engine.fol2sat.FOL2BoolTranslator$2.visit(FOL2BoolTranslator.java:126)
kodkod.ast.MultiplicityFormula.accept(MultiplicityFormula.java:94)
kodkod.engine.fol2sat.FOL2BoolTranslator.translate(FOL2BoolTranslator.java:138)
kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:837)
kodkod.engine.fol2sat.Translator.translate(Translator.java:630)
kodkod.engine.fol2sat.Translator.translate(Translator.java:174)
kodkod.engine.SolutionIterator.<init>(SolutionIterator.java:34)
kodkod.engine.Solver.solveAll(Solver.java:187)
edu.mit.csail.sdg.translator.A4Solution.solve(A4Solution.java:1482)
edu.mit.csail.sdg.translator.TranslateAlloyToKodkod.execute_commandFromBook(TranslateAlloyToKodkod.java:575)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:684)
edu.mit.csail.sdg.alloy4.WorkerEngine$5.run(WorkerEngine.java:468)
java.base/java.lang.Thread.run(Unknown Source)

[SteveZhangBit]

Thanks for pointing out the issue. The reason is that Int is a special set in the translation process. It is defined as a boolean constant (True), which means there is no way to minimize the set Int. By default, Alloy adds Int = {-8, -6, ..., 7} to the universe of a problem. Users have to manually pick the best range that fits their problems.

A quick fix is to check that for any minsome/maxsome r, r should be a boolean formula, and ignore this kind of usage.