The skolemization analysis finds the existential quantifiers that can be safely replace by constants + *
The skolemization analysis finds the existential quantifiers that can be safely replaced by constants * (Skolemizable). This class is not a pure analysis but a transformer, that is, it modifies an argument expression. * Additionally, this analysis finds the cardinality comparisons like Cardinality(S) >= 4 that can be checked * more optimally than the direct computation of the cardinalities.
@@ -22,7 +21,6 @@ import at.forsyte.apalache.tla.lir.values.TlaInt * @author Igor Konnov */ class SkolemizationMarker @Inject() (tracker: TransformationTracker) extends TlaExTransformation with LazyLogging { - override def apply(e: TlaEx): TlaEx = { transform(e) } @@ -58,12 +56,41 @@ class SkolemizationMarker @Inject() (tracker: TransformationTracker) extends Tla // Effectively, IF-THEN-ELSE requires both \E and \A forms case ex @ LetInEx(body, defs @ _*) => - // at this point, we only have nullary let-in definitions - def mapDef(df: TlaOperDecl) = df.copy(body = transform(df.body)) + // At this point, we only have nullary let-in definitions of the form: `LET A == e1 in e2` + // + // There are two important cases to distinguish (bugfix for #985): + // 1. Expression e1 contains `\E x \in S: P` and `A` is used in a positive form in `e2` (as a non-value). + // 2. Expression e1 contains `\E x \in S: P` and `A` is used in a negative form or as a value in `e2`. + // + // Hence, we create copies of A for the both cases: one that could be skolemized and one that could not be. + def skolemizeDef(df: TlaOperDecl): Option[TlaOperDecl] = { + df.typeTag match { + case Typed(OperT1(Seq(), BoolT1())) => + // Only if the let-definition returns a Boolean value, we have to worry about skolemization + Some(df.copy(body = transform(df.body), name = mkSkolemName(df.name))) + + case _ => + None + } + + } - LetInEx(transform(body), defs map mapDef: _*)(ex.typeTag) + // introduce skolemized copies of the operators that return a Boolean, if needed + LetInEx(transform(body), defs ++ defs.flatMap(skolemizeDef): _*)(ex.typeTag) - case ex @ OperEx(oper, args @ _*) => + case ex @ OperEx(TlaOper.apply, nm @ NameEx(operName)) => + ex.typeTag match { + case Typed(BoolT1()) => + // An application of a let-definition that returns a Boolean value. + // As Skolemization is allowed in this context, we use the Skolemizable version of the definition. + OperEx(TlaOper.apply, NameEx(mkSkolemName(operName))(nm.typeTag))(ex.typeTag) + + case _ => + // non-Boolean values are kept as they are + ex + } + + case ex @ OperEx(_, _ @_*) => // bugfix for #148: do not descend into value expressions, as Skolemization of non-formulas is unsound ex @@ -71,4 +98,8 @@ class SkolemizationMarker @Inject() (tracker: TransformationTracker) extends Tla terminal // terminal expression, stop here } + private def mkSkolemName(name: String): String = { + "%s$_skolem".format(name) + } + } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/analyses/TestSkolemizationMarker.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/analyses/TestSkolemizationMarker.scala index 199e1dc9e2..1170312b7f 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/analyses/TestSkolemizationMarker.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/analyses/TestSkolemizationMarker.scala @@ -1,8 +1,9 @@ -package at.forsyte.apalache.tla.bmcmt.analyses +package at.forsyte.apalache.bmcmt.analyses -import at.forsyte.apalache.tla.lir.OperEx -import at.forsyte.apalache.tla.lir.convenience.tla -import at.forsyte.apalache.tla.lir.oper.ApalacheOper +import at.forsyte.apalache.tla.bmcmt.analyses.SkolemizationMarker +import at.forsyte.apalache.tla.bmcmt.types.BoolT +import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, OperT1, SetT1} +import at.forsyte.apalache.tla.lir.TypedPredefs.{BuilderExAsTyped, BuilderOperDeclAsTyped} import at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners import at.forsyte.apalache.tla.lir.UntypedPredefs._ import org.junit.runner.RunWith @@ -11,6 +12,14 @@ import org.scalatest.{BeforeAndAfterEach, FunSuite} @RunWith(classOf[JUnitRunner]) class TestSkolemizationMarker extends FunSuite with BeforeAndAfterEach { + + import at.forsyte.apalache.tla.lir.convenience.tla._ + + private val Int = IntT1() + private val Bool = BoolT1() + private val BoolOper0 = OperT1(Seq(), BoolT1()) + private val IntSet = SetT1(IntT1()) + private var marker = new SkolemizationMarker(TrackerWithListeners()) override def beforeEach(): Unit = { @@ -18,18 +27,18 @@ class TestSkolemizationMarker extends FunSuite with BeforeAndAfterEach { } test("""mark: \E y \in S: P""") { - val input = tla.exists(tla.name("y"), tla.name("S"), tla.name("P")).untyped() - val expected = tla.apalacheSkolem(input).untyped() + val input = exists(name("y"), name("S"), name("P")).untyped() + val expected = apalacheSkolem(input).untyped() val output = marker(input) assert(expected == output) } test("""mark: \E y \in S: P /\ \E z \in S: Q""") { - val left = tla.exists(tla.name("y"), tla.name("S"), tla.name("P")) - val right = tla.exists(tla.name("z"), tla.name("S"), tla.name("Q")) - val input = tla.and(left, right).untyped() - val expected = tla.and(tla.apalacheSkolem(left), tla.apalacheSkolem(right)).untyped() + val left = exists(name("y"), name("S"), name("P")) + val right = exists(name("z"), name("S"), name("Q")) + val input = and(left, right).untyped() + val expected = and(apalacheSkolem(left), apalacheSkolem(right)).untyped() val output = marker(input) assert(expected == output) @@ -38,27 +47,66 @@ class TestSkolemizationMarker extends FunSuite with BeforeAndAfterEach { // see the issue #148 test("""no mark: x' <- \E y \in S: P""") { val input = - tla.assignPrime(tla.name("x"), tla.exists(tla.name("y"), tla.name("S"), tla.name("P"))).untyped() + assignPrime(name("x"), exists(name("y"), name("S"), name("P"))).untyped() val output = marker(input) assert(input == output) } + // skolemize let-definitions, if they are used positively as part of a formula, see the issue #985 + test("""mark: LET A == \E y \in S: P IN A \/ TRUE""") { + val bodyOfA = exists(name("y") as Int, name("S") as IntSet, name("P") as Bool) as Bool + val declOfA = declOp("A", bodyOfA) as BoolOper0 + val A = name("A") as BoolOper0 + val B = bool(true).typed() + val input = letIn(or(appOp(A) as Bool, B) as Bool, declOfA) as Bool + + // the body of A is skolemized + val bodyOfAskolem = apalacheSkolem(bodyOfA) as Bool + // the skolemized copy of A is used + val declOfAskolem = declOp("A$_skolem", bodyOfAskolem) as BoolOper0 + // note that we have two let-in definitions now: one that is skolemized and one that is not skolemized + val skolemA = name("A$_skolem") as BoolOper0 + val expected = letIn(or(appOp(skolemA) as Bool, B) as Bool, declOfA, declOfAskolem) as Bool + + val output = marker(input) + assert(expected == output) + } + + // do not skolemize let-definitions, if they are used as a value, see the issue #985 + test("""mark: LET A == \E y \in S: P IN A = FALSE""") { + val bodyOfA = exists(name("y") as Int, name("S") as IntSet, name("P") as Bool) as Bool + val declOfA = declOp("A", bodyOfA) as BoolOper0 + val A = name("A") as BoolOper0 + val B = bool(false).typed() + val input = letIn(eql(appOp(A) as Bool, B) as Bool, declOfA) as Bool + + // the body of A is skolemized + val bodyOfAskolem = apalacheSkolem(bodyOfA) as Bool + // the skolemized copy of A is used + val declOfAskolem = declOp("A$_skolem", bodyOfAskolem) as BoolOper0 + // note that we have two let-in definitions now: one that is skolemized and one that is not skolemized + val expected = letIn(eql(appOp(A) as Bool, B) as Bool, declOfA, declOfAskolem) as Bool + + val output = marker(input) + assert(expected == output) + } + test("""mark: Cardinality(S) >= 3""") { - val input = tla.ge(tla.card(tla.name("S")), tla.int(3)).untyped() - val expected = tla.apalacheConstCard(input).untyped() + val input = ge(card(name("S")), int(3)).untyped() + val expected = apalacheConstCard(input).untyped() val output = marker(input) assert(expected == output) } test("""no mark: ~(Cardinality(S) >= 3)""") { - val input = tla.not(tla.ge(tla.card(tla.name("S")), tla.int(3))).untyped() + val input = not(ge(card(name("S")), int(3))).untyped() val output = marker(input) assert(input == output) } test("""no mark: Cardinality(S) < 3""") { - val input = tla.lt(tla.card(tla.name("S")), tla.int(3)).untyped() + val input = lt(card(name("S")), int(3)).untyped() val output = marker(input) assert(input == output) }