Miniscoping requires NNF

[nancyday]

fortress -i --compiler MaxUnboundedScopes -t 3600 expert-models/3zltn65gds66b6f4q3lvbtgdkb6snmuu-alloy/fullsub2_SameFinalStates.smttc

Gets error message:

Exception in thread "main" fortress.util.Errors$Internal$PreconditionError: Miniscoping requires NNF (implications, iff, distinct eliminated) at fortress.util.Errors$Internal$.preconditionFailed(Errors.scala:65) at fortress.operations.NormalForms$Miniscoping$$anonfun$1.applyOrElse(NormalForms.scala:150) at fortress.operations.NormalForms$Miniscoping$$anonfun$1.applyOrElse(NormalForms.scala:84) at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35) This does not happen with the StandardCompiler (which I expect timesout), but I’m not sure why an unbound scope would trigger this?

From Ryan: Is it possible that the unbound scope resulted in an implication/iff/distinct not being eliminated?

[ryandancy]

This bug is caused by a combination of several factors:

• NnfTransformer doesn't recurse into ITEs, and so doesn't eliminate implications/iff/distinct inside ITEs.
• NormalForms.Miniscoping (called by SimplifyWithScalarQuantifiersTransformer) does recurse into ITEs and expects there to be no implications/iff/distinct.
• IntOPFITransformer seems to also eliminate iff (but perhaps not implications? @otzzila), but...
• MaxUnboundedScopesTransformer is eliminating the scope on IntSort, causing IntOPFITransformer not to run.
• Portus generates this particular model with an iff inside an ITE condition inside a definition returning Int (from the sum definitions optimization), so if-lifting doesn't eliminate the ITE.

As a quick fix you can replace line 19 in MaxUnboundedScopesTransformer with the following to preserve the scopes of builtin sorts like IntSort:

val new_scopes = scopes.filter { case (sort, scope) =>
    scope.isFixed() || sort.isBuiltin
}

(Note that even with this fix, the issue from #104 prevents fullsub2.als from working with -compiler MaxUnboundedScopes.)

I will figure out a better fix for the bug.