diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/DomainSize.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/DomainSize.java new file mode 100644 index 0000000000..6fc4943a5d --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/DomainSize.java @@ -0,0 +1,101 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.type; + +import com.google.common.base.Objects; + +import java.math.BigInteger; +import java.util.function.BinaryOperator; + +import static com.google.common.base.Preconditions.checkArgument; + +public class DomainSize { + + private final BigInteger finiteSize; + + private DomainSize(BigInteger value) { + finiteSize = value; + } + + public static DomainSize of(BigInteger val) { + checkArgument(val.signum() != -1, "DomainSize can't be negative"); + return new DomainSize(val); + } + + public static DomainSize of(long val) { + return of(BigInteger.valueOf(val)); + } + + public static final DomainSize INFINITY = new DomainSize(BigInteger.valueOf(-1)); + public static final DomainSize ZERO = of(0); + public static final DomainSize ONE = of(1); + public static final DomainSize TWO = of(2); + + private static DomainSize infiniteForAnyInfiniteApplyElse(DomainSize left, DomainSize right, BinaryOperator operator) { + if (left.isInfinite() || right.isInfinite()) + return INFINITY; + return of(operator.apply(left.finiteSize, right.finiteSize)); + } + + public boolean isInfinite() { + return equals(INFINITY); + } + + public boolean isBiggerThan(long limit) { + return this.equals(INFINITY) || finiteSize.compareTo(BigInteger.valueOf(limit)) > 0; + } + + public BigInteger getFiniteSize() { + return finiteSize; + } + + public static DomainSize add(DomainSize left, DomainSize right) { + return infiniteForAnyInfiniteApplyElse(left, right, BigInteger::add); + } + + public static DomainSize multiply(DomainSize left, DomainSize right) { + return infiniteForAnyInfiniteApplyElse(left, right, BigInteger::multiply); + } + + /** + * Raises a domain size to the power of the other. Returns {@link DomainSize#INFINITY} if either + * parameter is infinite or exponent is too large ( = can't fit into an integer) + */ + public static DomainSize pow(DomainSize base, DomainSize exponent) { + if (base.isInfinite() || exponent.isInfinite()) + return INFINITY; + int iExp; + try { + iExp = exponent.finiteSize.intValueExact(); + } catch (ArithmeticException exception) { + return INFINITY; + } + return of(base.finiteSize.pow(iExp)); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + DomainSize that = (DomainSize) o; + return Objects.equal(finiteSize, that.finiteSize); + } + + @Override + public int hashCode() { + return Objects.hashCode(finiteSize); + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/Type.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/Type.java index fe0d16d848..aad3f12198 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/Type.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/Type.java @@ -16,5 +16,5 @@ package hu.bme.mit.theta.core.type; public interface Type { - + DomainSize getDomainSize(); } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayType.java index 8be5b8bf26..db47723188 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayType.java @@ -15,15 +15,16 @@ */ package hu.bme.mit.theta.core.type.arraytype; -import static com.google.common.base.Preconditions.checkNotNull; - import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.abstracttype.EqExpr; import hu.bme.mit.theta.core.type.abstracttype.Equational; import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; +import static com.google.common.base.Preconditions.checkNotNull; + public final class ArrayType implements Equational> { @@ -97,4 +98,9 @@ public String toString() { final String indexString = String.format("([%s] -> %s)", indexType, elemType); return Utils.lispStringBuilder(TYPE_LABEL).add(indexString).toString(); } + + @Override + public DomainSize getDomainSize() { + return DomainSize.pow(elemType.getDomainSize(), indexType.getDomainSize()); + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/booltype/BoolType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/booltype/BoolType.java index c5373db970..4246eed7dc 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/booltype/BoolType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/booltype/BoolType.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.core.type.booltype; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.abstracttype.Equational; import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; @@ -59,4 +60,9 @@ public NeqExpr Neq(final Expr leftOp, final Expr r return BoolExprs.Xor(leftOp, rightOp); } + @Override + public DomainSize getDomainSize() { + return DomainSize.TWO; + } + } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java index be3e91e1c4..c9739a79c2 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java @@ -17,31 +17,15 @@ package hu.bme.mit.theta.core.type.bvtype; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.abstracttype.AddExpr; -import hu.bme.mit.theta.core.type.abstracttype.Additive; -import hu.bme.mit.theta.core.type.abstracttype.Castable; -import hu.bme.mit.theta.core.type.abstracttype.DivExpr; -import hu.bme.mit.theta.core.type.abstracttype.Divisible; -import hu.bme.mit.theta.core.type.abstracttype.EqExpr; -import hu.bme.mit.theta.core.type.abstracttype.Equational; -import hu.bme.mit.theta.core.type.abstracttype.GeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.GtExpr; -import hu.bme.mit.theta.core.type.abstracttype.LeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.LtExpr; -import hu.bme.mit.theta.core.type.abstracttype.ModExpr; -import hu.bme.mit.theta.core.type.abstracttype.MulExpr; -import hu.bme.mit.theta.core.type.abstracttype.Multiplicative; -import hu.bme.mit.theta.core.type.abstracttype.NegExpr; -import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.Ordered; -import hu.bme.mit.theta.core.type.abstracttype.PosExpr; -import hu.bme.mit.theta.core.type.abstracttype.RemExpr; -import hu.bme.mit.theta.core.type.abstracttype.SubExpr; +import hu.bme.mit.theta.core.type.abstracttype.*; import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; import hu.bme.mit.theta.core.type.fptype.FpType; +import java.math.BigInteger; + import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkState; import static hu.bme.mit.theta.core.type.fptype.FpExprs.FromBv; @@ -223,4 +207,9 @@ public GeqExpr Geq(Expr leftOp, Expr rightOp) { return BvExprs.UGeq(leftOp, rightOp); } } + + @Override + public DomainSize getDomainSize() { + return DomainSize.of(BigInteger.TWO.pow(size)); + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumEqExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumEqExpr.java new file mode 100644 index 0000000000..d5b61d9cb2 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumEqExpr.java @@ -0,0 +1,78 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.type.enumtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; + +public class EnumEqExpr extends EqExpr { + + private static final int HASH_SEED = 5326; + private static final String OPERATOR_LABEL = "="; + + private EnumEqExpr(Expr leftOp, Expr rightOp) { + super(leftOp, rightOp); + } + + public static EnumEqExpr of(Expr leftOp, Expr rightOp) { + return new EnumEqExpr(leftOp, rightOp); + } + + @Override + public BinaryExpr with(Expr leftOp, Expr rightOp) { + if (leftOp == getLeftOp() && rightOp == getRightOp()) { + return this; + } else { + return EnumEqExpr.of(leftOp, rightOp); + } + } + + @Override + public BinaryExpr withLeftOp(Expr leftOp) { + return with(leftOp, getRightOp()); + } + + @Override + public BinaryExpr withRightOp(Expr rightOp) { + return with(getLeftOp(), rightOp); + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } + + @Override + public BoolType getType() { + return Bool(); + } + + @Override + public LitExpr eval(Valuation val) { + return EnumLitExpr.eq((EnumLitExpr) getLeftOp().eval(val), (EnumLitExpr) getRightOp().eval(val)); + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumLitExpr.java new file mode 100644 index 0000000000..e6382574c1 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumLitExpr.java @@ -0,0 +1,78 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.type.enumtype; + +import com.google.common.base.Objects; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.NullaryExpr; +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; + +import static com.google.common.base.Preconditions.checkArgument; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; + +public final class EnumLitExpr extends NullaryExpr implements LitExpr { + + private final EnumType type; + private final String value; + + private EnumLitExpr(EnumType type, String value) { + this.type = type; + this.value = value; + } + + public static EnumLitExpr of(EnumType type, String literalName) { + String value = EnumType.getShortName(literalName); + checkArgument(type.getValues().contains(value), "Invalid value %s for type %s", value, type.getName()); + return new EnumLitExpr(type, value); + } + + @Override + public EnumType getType() { + return type; + } + + public String getValue() { + return value; + } + + @Override + public LitExpr eval(Valuation val) { + return this; + } + + @Override + public String toString() { + return EnumType.makeLongName(type.getName(), value); + } + + public static BoolLitExpr eq(EnumLitExpr l, EnumLitExpr r) { + return Bool(l.type.equals(r.type) && l.value.equals(r.value)); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + EnumLitExpr that = (EnumLitExpr) o; + return Objects.equal(type, that.type) && Objects.equal(value, that.value); + } + + @Override + public int hashCode() { + return Objects.hashCode(type, value); + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumNeqExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumNeqExpr.java new file mode 100644 index 0000000000..27bc44a945 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumNeqExpr.java @@ -0,0 +1,77 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.type.enumtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; + +public final class EnumNeqExpr extends NeqExpr { + + private static final int HASH_SEED = 7212; + private static final String OPERATOR_LABEL = "!="; + + private EnumNeqExpr(Expr leftOp, Expr rightOp) { + super(leftOp, rightOp); + } + public static EnumNeqExpr of(Expr leftOp, Expr rightOp) { + return new EnumNeqExpr(leftOp, rightOp); + } + + @Override + public BinaryExpr with(Expr leftOp, Expr rightOp) { + if (leftOp == getLeftOp() && rightOp == getRightOp()) { + return this; + } else { + return EnumNeqExpr.of(leftOp, rightOp); + } + } + + @Override + public BinaryExpr withLeftOp(Expr leftOp) { + return with(leftOp, getRightOp()); + } + + @Override + public BinaryExpr withRightOp(Expr rightOp) { + return with(getLeftOp(), rightOp); + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } + + @Override + public BoolType getType() { + return Bool(); + } + + @Override + public LitExpr eval(Valuation val) { + return null; + } +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumType.java new file mode 100644 index 0000000000..cedabacb68 --- /dev/null +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumType.java @@ -0,0 +1,91 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.type.enumtype; + +import hu.bme.mit.theta.core.type.DomainSize; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.type.abstracttype.Equational; +import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; + +import java.util.Collection; +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Set; + +import static com.google.common.base.Preconditions.checkArgument; + +public final class EnumType implements Equational, Type { + + public static final String FULLY_QUALIFIED_NAME_SEPARATOR = "."; + private int counter = 0; + private final Map literals; + private final String name; + + private EnumType(String name, Collection values) { + this.name = name; + this.literals = new LinkedHashMap<>(); + values.forEach(value -> literals.put(value, counter++)); + } + + public static EnumType of(String name, Collection values) { + return new EnumType(name, values); + } + + public static String makeLongName(String typeName, String literal) { + return String.format("%s%s%s", typeName, FULLY_QUALIFIED_NAME_SEPARATOR, literal); + } + + public static String makeLongName(EnumType type, String literal) { + return makeLongName(type.getName(), literal); + } + + public static String getShortName(String longName) { + if (!longName.contains(FULLY_QUALIFIED_NAME_SEPARATOR)) + return longName; + return longName.substring(longName.indexOf(FULLY_QUALIFIED_NAME_SEPARATOR) + FULLY_QUALIFIED_NAME_SEPARATOR.length()); + } + + @Override + public DomainSize getDomainSize() { + return DomainSize.of(literals.size()); + } + + @Override + public EqExpr Eq(Expr leftOp, Expr rightOp) { + return EnumEqExpr.of(leftOp, rightOp); + } + + @Override + public NeqExpr Neq(Expr leftOp, Expr rightOp) { + return EnumNeqExpr.of(leftOp, rightOp); + } + + public Set getValues() { + return literals.keySet(); + } + + public String getName() { + return name; + } + + public int getIntValue(String literal) { + checkArgument(literals.containsKey(literal), String.format("Enum type %s does not contain literal '%s'", name, literal)); + return literals.get(literal); + } + +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java index 911d879340..e32c037a67 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java @@ -16,23 +16,11 @@ package hu.bme.mit.theta.core.type.fptype; import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.abstracttype.AddExpr; -import hu.bme.mit.theta.core.type.abstracttype.Additive; -import hu.bme.mit.theta.core.type.abstracttype.DivExpr; -import hu.bme.mit.theta.core.type.abstracttype.EqExpr; -import hu.bme.mit.theta.core.type.abstracttype.Equational; -import hu.bme.mit.theta.core.type.abstracttype.GeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.GtExpr; -import hu.bme.mit.theta.core.type.abstracttype.LeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.LtExpr; -import hu.bme.mit.theta.core.type.abstracttype.MulExpr; -import hu.bme.mit.theta.core.type.abstracttype.Multiplicative; -import hu.bme.mit.theta.core.type.abstracttype.NegExpr; -import hu.bme.mit.theta.core.type.abstracttype.NeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.Ordered; -import hu.bme.mit.theta.core.type.abstracttype.PosExpr; -import hu.bme.mit.theta.core.type.abstracttype.SubExpr; +import hu.bme.mit.theta.core.type.abstracttype.*; + +import java.math.BigInteger; import static com.google.common.base.Preconditions.checkArgument; @@ -155,4 +143,9 @@ public GtExpr Gt(Expr leftOp, Expr rightOp) { public GeqExpr Geq(Expr leftOp, Expr rightOp) { return FpExprs.Geq(leftOp, rightOp); } + + @Override + public DomainSize getDomainSize() { + return DomainSize.of(BigInteger.TWO.pow(significand).multiply(BigInteger.TWO.pow(exponent))); + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncType.java index 0e3b7526cd..d9fe54b37b 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncType.java @@ -15,11 +15,12 @@ */ package hu.bme.mit.theta.core.type.functype; -import static com.google.common.base.Preconditions.checkNotNull; - import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Type; +import static com.google.common.base.Preconditions.checkNotNull; + public final class FuncType implements Type { private final static int HASH_SEED = 3931; @@ -78,4 +79,8 @@ public String toString() { return Utils.lispStringBuilder(TYPE_LABEL).add(paramType).add(resultType).toString(); } + @Override + public DomainSize getDomainSize() { + throw new UnsupportedOperationException(); + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java index 2472127f31..ee2b55d5f3 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntType.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.core.type.inttype; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.abstracttype.*; @@ -133,4 +134,9 @@ public Expr Cast(final Expr op, throw new ClassCastException("Int cannot be cast to " + type); } } + + @Override + public DomainSize getDomainSize() { + return DomainSize.INFINITY; + } } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java index d3a9f12551..5a79f97c3f 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.core.type.rattype; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.abstracttype.Additive; import hu.bme.mit.theta.core.type.abstracttype.Equational; @@ -112,4 +113,8 @@ public RatGeqExpr Geq(final Expr leftOp, final Expr rightOp) { return RatExprs.Geq(leftOp, rightOp); } + @Override + public DomainSize getDomainSize() { + return DomainSize.INFINITY; + } } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index dacf64971c..a95dfa69e0 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -18,11 +18,7 @@ import com.google.common.cache.Cache; import com.google.common.cache.CacheBuilder; import com.google.common.collect.ImmutableList; -import com.microsoft.z3.BitVecExpr; -import com.microsoft.z3.BoolExpr; -import com.microsoft.z3.Context; -import com.microsoft.z3.FPExpr; -import com.microsoft.z3.FPSort; +import com.microsoft.z3.*; import hu.bme.mit.theta.common.DispatchTable; import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.dsl.Env; @@ -34,114 +30,18 @@ import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; -import hu.bme.mit.theta.core.type.booltype.AndExpr; -import hu.bme.mit.theta.core.type.booltype.ExistsExpr; -import hu.bme.mit.theta.core.type.booltype.FalseExpr; -import hu.bme.mit.theta.core.type.booltype.ForallExpr; -import hu.bme.mit.theta.core.type.booltype.IffExpr; -import hu.bme.mit.theta.core.type.booltype.ImplyExpr; -import hu.bme.mit.theta.core.type.booltype.NotExpr; -import hu.bme.mit.theta.core.type.booltype.OrExpr; -import hu.bme.mit.theta.core.type.booltype.TrueExpr; -import hu.bme.mit.theta.core.type.booltype.XorExpr; -import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; -import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; -import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr; -import hu.bme.mit.theta.core.type.bvtype.BvEqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; -import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; -import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvMulExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; -import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; -import hu.bme.mit.theta.core.type.bvtype.BvPosExpr; -import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; -import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSGtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSLtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; -import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; -import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvUGtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvULeqExpr; -import hu.bme.mit.theta.core.type.bvtype.BvULtExpr; -import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; -import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; -import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; -import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; -import hu.bme.mit.theta.core.type.fptype.FpAddExpr; -import hu.bme.mit.theta.core.type.fptype.FpAssignExpr; -import hu.bme.mit.theta.core.type.fptype.FpDivExpr; -import hu.bme.mit.theta.core.type.fptype.FpEqExpr; -import hu.bme.mit.theta.core.type.fptype.FpFromBvExpr; -import hu.bme.mit.theta.core.type.fptype.FpGeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpGtExpr; -import hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr; -import hu.bme.mit.theta.core.type.fptype.FpIsNanExpr; -import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpLitExpr; -import hu.bme.mit.theta.core.type.fptype.FpLtExpr; -import hu.bme.mit.theta.core.type.fptype.FpMaxExpr; -import hu.bme.mit.theta.core.type.fptype.FpMinExpr; -import hu.bme.mit.theta.core.type.fptype.FpMulExpr; -import hu.bme.mit.theta.core.type.fptype.FpNegExpr; -import hu.bme.mit.theta.core.type.fptype.FpNeqExpr; -import hu.bme.mit.theta.core.type.fptype.FpPosExpr; -import hu.bme.mit.theta.core.type.fptype.FpRemExpr; -import hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr; -import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; -import hu.bme.mit.theta.core.type.fptype.FpSqrtExpr; -import hu.bme.mit.theta.core.type.fptype.FpSubExpr; -import hu.bme.mit.theta.core.type.fptype.FpToBvExpr; -import hu.bme.mit.theta.core.type.fptype.FpToFpExpr; +import hu.bme.mit.theta.core.type.arraytype.*; +import hu.bme.mit.theta.core.type.booltype.*; +import hu.bme.mit.theta.core.type.bvtype.*; +import hu.bme.mit.theta.core.type.enumtype.EnumEqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumNeqExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; +import hu.bme.mit.theta.core.type.fptype.*; import hu.bme.mit.theta.core.type.functype.FuncAppExpr; import hu.bme.mit.theta.core.type.functype.FuncType; -import hu.bme.mit.theta.core.type.inttype.IntAddExpr; -import hu.bme.mit.theta.core.type.inttype.IntDivExpr; -import hu.bme.mit.theta.core.type.inttype.IntEqExpr; -import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntGtExpr; -import hu.bme.mit.theta.core.type.inttype.IntLeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntLitExpr; -import hu.bme.mit.theta.core.type.inttype.IntLtExpr; -import hu.bme.mit.theta.core.type.inttype.IntModExpr; -import hu.bme.mit.theta.core.type.inttype.IntMulExpr; -import hu.bme.mit.theta.core.type.inttype.IntNegExpr; -import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; -import hu.bme.mit.theta.core.type.inttype.IntPosExpr; -import hu.bme.mit.theta.core.type.inttype.IntRemExpr; -import hu.bme.mit.theta.core.type.inttype.IntSubExpr; -import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; -import hu.bme.mit.theta.core.type.rattype.RatAddExpr; -import hu.bme.mit.theta.core.type.rattype.RatDivExpr; -import hu.bme.mit.theta.core.type.rattype.RatEqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatGtExpr; -import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatLitExpr; -import hu.bme.mit.theta.core.type.rattype.RatLtExpr; -import hu.bme.mit.theta.core.type.rattype.RatMulExpr; -import hu.bme.mit.theta.core.type.rattype.RatNegExpr; -import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; -import hu.bme.mit.theta.core.type.rattype.RatPosExpr; -import hu.bme.mit.theta.core.type.rattype.RatSubExpr; -import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; +import hu.bme.mit.theta.core.type.inttype.*; +import hu.bme.mit.theta.core.type.rattype.*; import hu.bme.mit.theta.core.utils.BvUtils; import java.util.List; @@ -400,6 +300,14 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex .addCase(ArrayInitExpr.class, this::transformArrayInit) + // Enums + + .addCase(EnumLitExpr.class, this::transformEnumLit) + + .addCase(EnumEqExpr.class, this::transformEnumEq) + + .addCase(EnumNeqExpr.class, this::transformEnumNeq) + .build(); } @@ -1241,6 +1149,23 @@ private com.microsoft.z3.Expr transformFuncApp(final FuncAppExpr expr) { } } + private com.microsoft.z3.Expr transformEnumLit(final EnumLitExpr expr) { + EnumType enumType = expr.getType(); + return ((EnumSort) transformer.toSort(enumType)).getConst(enumType.getIntValue(expr.getValue())); + } + + private com.microsoft.z3.Expr transformEnumEq(final EnumEqExpr expr) { + final com.microsoft.z3.Expr leftOpTerm = toTerm(expr.getLeftOp()); + final com.microsoft.z3.Expr rightOpTerm = toTerm(expr.getRightOp()); + return context.mkEq(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformEnumNeq(final EnumNeqExpr expr) { + final com.microsoft.z3.Expr leftOpTerm = toTerm(expr.getLeftOp()); + final com.microsoft.z3.Expr rightOpTerm = toTerm(expr.getRightOp()); + return context.mkNot(context.mkEq(leftOpTerm, rightOpTerm)); + } + public void reset() { exprToTerm.invalidateAll(); } diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java index c1083760c6..9aeb84a8b7 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3Solver.java @@ -29,20 +29,14 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.functype.FuncType; -import hu.bme.mit.theta.solver.Solver; -import hu.bme.mit.theta.solver.SolverStatus; import hu.bme.mit.theta.solver.Stack; -import hu.bme.mit.theta.solver.UCSolver; -import hu.bme.mit.theta.solver.UnknownSolverStatusException; +import hu.bme.mit.theta.solver.*; import hu.bme.mit.theta.solver.impl.StackImpl; -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.LinkedList; -import java.util.Map; -import java.util.Optional; +import java.util.*; import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Preconditions.checkState; @@ -287,6 +281,8 @@ private LitExpr extractLiteral(final ConstDecl extractBvConstLiteral(final FuncDecl funcDecl) { } } + private LitExpr extractEnumLiteral(final ConstDecl constDecl, final FuncDecl funcDecl) { + return EnumLitExpr.of((EnumType) constDecl.getType(), z3Model.getConstInterp(funcDecl).toString()); + } + private LitExpr extractConstLiteral(final FuncDecl funcDecl) { final com.microsoft.z3.Expr term = z3Model.getConstInterp(funcDecl); if (term == null) { diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java index 3a21714269..bbe8ad3c64 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java @@ -16,12 +16,9 @@ package hu.bme.mit.theta.solver.z3; import com.google.common.collect.ImmutableList; -import com.microsoft.z3.ArrayExpr; -import com.microsoft.z3.ArraySort; -import com.microsoft.z3.FPNum; -import com.microsoft.z3.FuncDecl; -import com.microsoft.z3.Model; -import com.microsoft.z3.Z3Exception; +import com.microsoft.z3.*; +import com.microsoft.z3.enumerations.Z3_decl_kind; +import com.microsoft.z3.enumerations.Z3_sort_kind; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; @@ -30,25 +27,14 @@ import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.abstracttype.AddExpr; -import hu.bme.mit.theta.core.type.abstracttype.EqExpr; -import hu.bme.mit.theta.core.type.abstracttype.GeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.GtExpr; -import hu.bme.mit.theta.core.type.abstracttype.LeqExpr; -import hu.bme.mit.theta.core.type.abstracttype.LtExpr; -import hu.bme.mit.theta.core.type.abstracttype.MulExpr; +import hu.bme.mit.theta.core.type.abstracttype.*; import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; -import hu.bme.mit.theta.core.type.booltype.AndExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.booltype.FalseExpr; -import hu.bme.mit.theta.core.type.booltype.IffExpr; -import hu.bme.mit.theta.core.type.booltype.ImplyExpr; -import hu.bme.mit.theta.core.type.booltype.NotExpr; -import hu.bme.mit.theta.core.type.booltype.OrExpr; -import hu.bme.mit.theta.core.type.booltype.TrueExpr; +import hu.bme.mit.theta.core.type.booltype.*; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.functype.FuncType; @@ -74,18 +60,13 @@ import java.util.stream.Collectors; import java.util.stream.Stream; -import static com.google.common.base.Preconditions.checkArgument; -import static com.google.common.base.Preconditions.checkNotNull; -import static com.google.common.base.Preconditions.checkState; +import static com.google.common.base.Preconditions.*; import static com.google.common.collect.ImmutableList.toImmutableList; import static hu.bme.mit.theta.common.Utils.head; import static hu.bme.mit.theta.common.Utils.tail; import static hu.bme.mit.theta.core.decl.Decls.Param; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.BvType; import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func; @@ -271,6 +252,12 @@ private Expr transformFpLit(final com.microsoft.z3.Expr term) { return FpUtils.bigFloatToFpLitExpr(bigFloat, type); } + private Expr transformEnumLit(final com.microsoft.z3.Expr term, final EnumType enumType) { + String longName = term.getFuncDecl().getName().toString(); + String literal = EnumType.getShortName(longName); + return EnumLitExpr.of(enumType, literal); + } + private Expr transformApp(final com.microsoft.z3.Expr term, final Model model, final List> vars) { @@ -494,6 +481,22 @@ private TriFunction>, Expr> exprBi return (term, model, vars) -> { final com.microsoft.z3.Expr[] args = term.getArgs(); checkArgument(args.length == 2, "Number of arguments must be two"); + if (args[0].getSort().getSortKind().equals(Z3_sort_kind.Z3_DATATYPE_SORT)) { + // binary operator is on enum types + // if either arg is a literal, we need special handling to get its type + // (references' decl kind is Z3_OP_UNINTERPRETED, literals' decl kind is Z3_OP_DT_CONSTRUCTOR) + int litIndex = -1; + for (int i = 0; i < 2; i++) { + if (args[i].getFuncDecl().getDeclKind().equals(Z3_decl_kind.Z3_OP_DT_CONSTRUCTOR)) + litIndex = i; + } + if (litIndex > -1) { + int refIndex = Math.abs(litIndex - 1); + final Expr refOp = transform(args[refIndex], model, vars); + final Expr litExpr = transformEnumLit(args[litIndex], (EnumType) refOp.getType()); + return function.apply(refOp, litExpr); + } + } final Expr op1 = transform(args[0], model, vars); final Expr op2 = transform(args[1], model, vars); return function.apply(op1, op2); diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java index fa06b7f5c8..742429a830 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java @@ -17,17 +17,17 @@ import com.google.common.collect.Sets; import com.microsoft.z3.Context; +import com.microsoft.z3.EnumSort; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.rattype.RatType; -import java.util.Optional; -import java.util.Set; -import java.util.TreeSet; +import java.util.*; final class Z3TypeTransformer { @@ -40,6 +40,7 @@ final class Z3TypeTransformer { private final com.microsoft.z3.RealSort realSort; private final Set bvSorts; private final Set fpSorts; + private final Map enumSorts; Z3TypeTransformer(final Z3TransformationManager transformer, final Context context) { this.context = context; @@ -50,6 +51,7 @@ final class Z3TypeTransformer { realSort = context.mkRealSort(); bvSorts = Sets.synchronizedNavigableSet(new TreeSet<>()); fpSorts = Sets.synchronizedNavigableSet(new TreeSet<>()); + enumSorts = new HashMap<>(); } public com.microsoft.z3.Sort toSort(final Type type) { @@ -89,9 +91,11 @@ public com.microsoft.z3.Sort toSort(final Type type) { final com.microsoft.z3.Sort indexSort = toSort(arrayType.getIndexType()); final com.microsoft.z3.Sort elemSort = toSort(arrayType.getElemType()); return context.mkArraySort(indexSort, elemSort); - } else { + } else if (type instanceof EnumType enumType) { + return enumSorts.computeIfAbsent(enumType.getName(), key -> createEnumSort(enumType)); + }else { throw new UnsupportedOperationException( - "Unsupporte type: " + type.getClass().getSimpleName()); + "Unsupported type: " + type.getClass().getSimpleName()); } } @@ -99,4 +103,8 @@ public void reset() { bvSorts.clear(); } + private EnumSort createEnumSort(EnumType enumType) { + return context.mkEnumSort(enumType.getName(), enumType.getValues().stream().map(lit -> EnumType.makeLongName(enumType, lit)).toArray(String[]::new)); + } + } diff --git a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java index fbfb844627..dafe9e849e 100644 --- a/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java +++ b/subprojects/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java @@ -19,13 +19,10 @@ import hu.bme.mit.theta.analysis.expl.ExplState; import hu.bme.mit.theta.common.LispStringBuilder; import hu.bme.mit.theta.common.Utils; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.analysis.XstsState; import java.util.List; -import java.util.Optional; import static com.google.common.base.Preconditions.*; @@ -84,21 +81,9 @@ public String toString() { sb.add(Utils.lispStringBuilder(XstsState.class.getSimpleName()) .add(state.isInitialized() ? "post_init" : "pre_init") .add(state.lastActionWasEnv() ? "last_env" : "last_internal").body() - .add(stateToString(state.getState())).toString()); + .add(state.getState().toString())); } return sb.toString(); } - public String stateToString(ExplState state) { - final LispStringBuilder sb = Utils.lispStringBuilder(ExplState.class.getSimpleName()) - .body(); - for (VarDecl decl : xsts.getVars()) { - Optional val = state.eval(decl); - if (val.isPresent() && xsts.getVarToType().containsKey(decl)) { - sb.add(String.format("(%s %s)", decl.getName(), - xsts.getVarToType().get(decl).serializeLiteral(val.get()))); - } - } - return sb.toString(); - } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsEnumSemanticsTest.java similarity index 50% rename from subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java rename to subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsEnumSemanticsTest.java index 1d40f9a9b5..7a24971164 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsEnumSemanticsTest.java @@ -13,20 +13,25 @@ * See the License for the specific language governing permissions and * limitations under the License. */ -package hu.bme.mit.theta.xsts.type; +package hu.bme.mit.theta.xsts.analysis; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.xsts.dsl.XstsDslManager; +import org.junit.Test; -public interface XstsType { +import java.io.FileInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.io.SequenceInputStream; - T getType(); +public class XstsEnumSemanticsTest { - Expr createBoundExpr(final VarDecl decl); + @Test(expected = ClassCastException.class) + public void test() throws IOException { - String serializeLiteral(final LitExpr literal); + try (InputStream inputStream = new SequenceInputStream(new FileInputStream("src/test/resources/model/literals_bad.xsts"), + new FileInputStream("src/test/resources/property/literals.prop"))) { + XstsDslManager.createXsts(inputStream); + } + } } diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java index 3dcdf8e75b..c3409dc405 100644 --- a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java +++ b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java @@ -132,13 +132,13 @@ public static Collection data() { false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", - true, XstsConfigBuilder.Domain.PRED_CART}, + false, XstsConfigBuilder.Domain.PRED_CART}, {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", - true, XstsConfigBuilder.Domain.EXPL}, + false, XstsConfigBuilder.Domain.EXPL}, {"src/test/resources/model/literals.xsts", "src/test/resources/property/literals.prop", - true, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, + false, XstsConfigBuilder.Domain.EXPL_PRED_COMBINED}, {"src/test/resources/model/cross3.xsts", "src/test/resources/property/cross.prop", false, XstsConfigBuilder.Domain.PRED_CART}, diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/literals.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/literals.xsts index d7346a37dd..2c90cae3ff 100644 --- a/subprojects/xsts/xsts-analysis/src/test/resources/model/literals.xsts +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/literals.xsts @@ -1,8 +1,7 @@ -type first : { A, B, C, D } -type second : { D, C, B, A } +type alphabet : { A, B, C, D } -var f : first = A -var s : second = A +var f : alphabet = A +var g : alphabet = B trans {} diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/model/literals_bad.xsts b/subprojects/xsts/xsts-analysis/src/test/resources/model/literals_bad.xsts new file mode 100644 index 0000000000..f39e84ee5e --- /dev/null +++ b/subprojects/xsts/xsts-analysis/src/test/resources/model/literals_bad.xsts @@ -0,0 +1,11 @@ +type alphabet : { A, B, C, D } +type second_alphabet : { A, B, C, D } + +var f : alphabet = A +var g : second_alphabet = A + +trans {} + +init {} + +env {} \ No newline at end of file diff --git a/subprojects/xsts/xsts-analysis/src/test/resources/property/literals.prop b/subprojects/xsts/xsts-analysis/src/test/resources/property/literals.prop index 434d7eca1d..a775a9d572 100644 --- a/subprojects/xsts/xsts-analysis/src/test/resources/property/literals.prop +++ b/subprojects/xsts/xsts-analysis/src/test/resources/property/literals.prop @@ -1,3 +1,3 @@ prop { - f == s + f == g } \ No newline at end of file diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java index 4843ae72bf..b413828c01 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java @@ -22,16 +22,16 @@ import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.core.utils.StmtUtils; -import hu.bme.mit.theta.xsts.type.XstsType; -import java.util.*; +import java.util.Collection; +import java.util.Collections; +import java.util.Set; import static com.google.common.base.Preconditions.checkNotNull; public final class XSTS { private final Collection> vars; - private final Map, XstsType> varToType; private final Set> ctrlVars; private final NonDetStmt tran; @@ -49,10 +49,6 @@ public Collection> getVars() { return vars; } - public Map, XstsType> getVarToType() { - return varToType; - } - public Expr getProp() { return prop; } @@ -73,7 +69,7 @@ public Set> getCtrlVars() { return ctrlVars; } - public XSTS(final Map, XstsType> varToType, final Set> ctrlVars, + public XSTS(final Set> ctrlVars, final NonDetStmt init, final NonDetStmt tran, final NonDetStmt env, final Expr initFormula, final Expr prop) { this.tran = checkNotNull(tran); @@ -81,11 +77,9 @@ public XSTS(final Map, XstsType> varToType, final Set> this.env = checkNotNull(env); this.initFormula = checkNotNull(initFormula); this.prop = checkNotNull(prop); - this.varToType = varToType; this.ctrlVars = ctrlVars; final Set> tmpVars = Containers.createSet(); - tmpVars.addAll(varToType.keySet()); tmpVars.addAll(StmtUtils.getVars(tran)); tmpVars.addAll(StmtUtils.getVars(env)); tmpVars.addAll(StmtUtils.getVars(init)); diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/CustomTypeDeclarationUtil.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/CustomTypeDeclarationUtil.java new file mode 100644 index 0000000000..c0ecb7f62a --- /dev/null +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/CustomTypeDeclarationUtil.java @@ -0,0 +1,45 @@ +/* + * Copyright 2023 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.xsts.dsl; + +import hu.bme.mit.theta.common.dsl.DynamicScope; +import hu.bme.mit.theta.common.dsl.Env; +import hu.bme.mit.theta.common.dsl.Symbol; +import hu.bme.mit.theta.core.type.enumtype.EnumType; + +import java.util.Optional; + +public final class CustomTypeDeclarationUtil { + + private CustomTypeDeclarationUtil(){} + + public static void declareTypeWithShortName(DynamicScope currentScope, EnumType enumType, String literal, Env env) { + Symbol fullNameSymbol = currentScope.resolve(EnumType.makeLongName(enumType, literal)).orElseThrow(); + if (fullNameSymbol instanceof XstsCustomLiteralSymbol fNameCustLitSymbol) { + var customSymbol = XstsCustomLiteralSymbol.copyWithName(fNameCustLitSymbol, literal); + Optional optionalSymbol = currentScope.resolve(literal); + if (optionalSymbol.isPresent()) { + env.define(optionalSymbol.get(), customSymbol.instantiate()); + } else { + currentScope.declare(customSymbol); + env.define(customSymbol, customSymbol.instantiate()); + } + } else { + throw new IllegalArgumentException(String.format("%s is not a literal of type %s", literal, enumType.getName())); + } + } + +} diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java index 37153bfc73..995103c49d 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java @@ -17,37 +17,40 @@ import hu.bme.mit.theta.common.dsl.Symbol; import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.xsts.type.XstsCustomType; - -import java.math.BigInteger; - -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; public class XstsCustomLiteralSymbol implements Symbol { - private final XstsCustomType.XstsCustomLiteral literal; + private final EnumType type; - private static int counter = 0; + private final String literal; + + public XstsCustomLiteralSymbol(EnumType type, String literal) { + this.type = type; + this.literal = literal; + } - public XstsCustomLiteralSymbol(String name) { - this.literal = XstsCustomType.XstsCustomLiteral.of(name, BigInteger.valueOf(counter++)); + public static XstsCustomLiteralSymbol of(EnumType type, String literal) { + return new XstsCustomLiteralSymbol(type, literal); } @Override public String getName() { - return literal.getName(); + return literal; } @Override public String toString() { - return literal.toString(); + return literal; } public Expr instantiate() { - return Int(literal.getIntValue()); + return EnumLitExpr.of(type, EnumType.getShortName(literal)); } - public XstsCustomType.XstsCustomLiteral getLiteral() { - return literal; + public static XstsCustomLiteralSymbol copyWithName(XstsCustomLiteralSymbol symbol, String newName) { + return new XstsCustomLiteralSymbol(symbol.type, newName); } + } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java index dd3f5d968b..6e5337fdcf 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java @@ -17,34 +17,33 @@ import hu.bme.mit.theta.common.dsl.Symbol; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.xsts.type.XstsCustomType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import java.util.Objects; public final class XstsCustomTypeSymbol implements Symbol { - private XstsCustomType xstsType; + private final EnumType enumType; - private XstsCustomTypeSymbol(final XstsCustomType xstsType) { - this.xstsType = xstsType; + private XstsCustomTypeSymbol(final EnumType enumType) { + this.enumType = enumType; } - public static XstsCustomTypeSymbol of(final XstsCustomType xstsType) { + public static XstsCustomTypeSymbol of(final EnumType xstsType) { return new XstsCustomTypeSymbol(xstsType); } @Override public int hashCode() { - return Objects.hash(xstsType); + return Objects.hash(enumType); } @Override public boolean equals(final Object obj) { if (this == obj) { return true; - } else if (obj instanceof XstsCustomTypeSymbol) { - final XstsCustomTypeSymbol that = (XstsCustomTypeSymbol) obj; - return this.xstsType.equals(that.xstsType); + } else if (obj instanceof XstsCustomTypeSymbol that) { + return this.enumType.equals(that.enumType); } else { return false; } @@ -52,19 +51,15 @@ public boolean equals(final Object obj) { @Override public String toString() { - return xstsType.toString(); - } - - public XstsCustomType getXstsType() { - return xstsType; + return enumType.toString(); } @Override public String getName() { - return xstsType.getName(); + return enumType.getName(); } public Type instantiate() { - return xstsType.getType(); + return enumType; } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java index 6841f872f9..461708aa6f 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java @@ -25,16 +25,13 @@ import hu.bme.mit.theta.core.dsl.ParseException; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.abstracttype.AddExpr; -import hu.bme.mit.theta.core.type.abstracttype.DivExpr; -import hu.bme.mit.theta.core.type.abstracttype.ModExpr; -import hu.bme.mit.theta.core.type.abstracttype.MulExpr; -import hu.bme.mit.theta.core.type.abstracttype.RemExpr; -import hu.bme.mit.theta.core.type.abstracttype.SubExpr; +import hu.bme.mit.theta.core.type.abstracttype.*; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.core.type.booltype.FalseExpr; import hu.bme.mit.theta.core.type.booltype.TrueExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; import org.antlr.v4.runtime.Token; @@ -51,69 +48,15 @@ import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.common.Utils.head; import static hu.bme.mit.theta.common.Utils.tail; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Gt; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Leq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Lt; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mod; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mul; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neg; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Pos; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Rem; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.*; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Iff; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Xor; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.utils.ExprUtils.simplify; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AccessContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AccessorExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AdditiveExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.AndExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrLitExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrayReadAccessContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ArrayWriteAccessContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.DIV; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.EQ; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.EqualityExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.FalseExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.GEQ; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.GT; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IdExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IffExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ImplyExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IntLitExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.IteExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.LEQ; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.LT; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MINUS; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MOD; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MUL; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.MultiplicativeExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.NEQ; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.NotExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.OrExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.PLUS; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.ParenExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.REM; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.RelationExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.TrueExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.UnaryExprContext; -import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.XorExprContext; +import static hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; import static java.util.stream.Collectors.toList; final class XstsExpression { @@ -234,17 +177,29 @@ public Expr visitNotExpr(final NotExprContext ctx) { @Override public Expr visitEqualityExpr(final EqualityExprContext ctx) { if (ctx.rightOp != null) { - final Expr leftOp = ctx.leftOp.accept(this); - final Expr rightOp = ctx.rightOp.accept(this); - - switch (ctx.oper.getType()) { - case EQ: - return Eq(leftOp, rightOp); - case NEQ: - return Neq(leftOp, rightOp); - default: - throw new ParseException(ctx, "Unknown operator"); + Expr leftOp; + boolean inverse = false; + final Expr rightOp; + try { + leftOp = ctx.leftOp.accept(this); + } catch (ParseException e) { + // It's possible that the left side is an enum literal + // So we have to parse enum type from the right side first + leftOp = ctx.rightOp.accept(this); + inverse = true; + } + if (leftOp.getType() instanceof EnumType enumType) { + env.push(); + enumType.getValues().forEach(literal -> CustomTypeDeclarationUtil.declareTypeWithShortName(currentScope, enumType, literal, env)); } + rightOp = (inverse ? ctx.leftOp : ctx.rightOp).accept(this); + if (leftOp.getType() instanceof EnumType) + env.pop(); + return switch (ctx.oper.getType()) { + case EQ -> Eq(leftOp, rightOp); + case NEQ -> Neq(leftOp, rightOp); + default -> throw new ParseException(ctx, "Unknown operator"); + }; } else { return visitChildren(ctx); @@ -523,7 +478,7 @@ private Expr createArrayLitExpr( final T2 valueType; if (ctx.indexType != null) { - indexType = (T1) new XstsType(typeTable, ctx.indexType).instantiate(env).getType(); + indexType = (T1) new XstsType(typeTable, ctx.indexType).instantiate(env); } else { indexType = (T1) ctx.indexExpr.get(0).accept(this).getType(); } @@ -550,10 +505,9 @@ public Expr visitIdExpr(final IdExprContext ctx) { } final Symbol symbol = optSymbol.get(); final Object val = env.eval(symbol); - if (val instanceof IntLitExpr) { - return (IntLitExpr) val; - } else if (val instanceof Decl) { - final Decl decl = (Decl) val; + if (val instanceof EnumLitExpr enumLiteral) { + return enumLiteral; + } else if (val instanceof Decl decl) { return decl.getRef(); } throw new ParseException(ctx, diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java index 14bb7e1236..d244fd0a04 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java @@ -22,20 +22,18 @@ import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.utils.ExprUtils; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.XstsContext; -import hu.bme.mit.theta.xsts.type.XstsCustomType; -import hu.bme.mit.theta.xsts.type.XstsType; import java.util.*; import java.util.regex.Pattern; -import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.*; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; public class XstsSpecification implements DynamicScope { @@ -43,6 +41,7 @@ public class XstsSpecification implements DynamicScope { private final SymbolTable symbolTable; private final SymbolTable typeTable; private final XstsContext context; + private final Set customTypeShortNames; private final Pattern tempVarPattern = Pattern.compile("temp([0-9])+"); @@ -50,6 +49,7 @@ public XstsSpecification(XstsContext context) { this.context = checkNotNull(context); this.symbolTable = new SymbolTable(); this.typeTable = new SymbolTable(); + customTypeShortNames = Containers.createSet(); } @Override @@ -65,41 +65,40 @@ public Optional resolve(String name) { public XSTS instantiate() { final Env env = new Env(); - final Map, XstsType> varToType = Containers.createMap(); final Set> ctrlVars = Containers.createSet(); final List> initExprs = new ArrayList<>(); for (var typeDeclContext : context.typeDeclarations) { - final List literalSymbols = new ArrayList<>(); - for (var literalContext : typeDeclContext.literals) { - var optSymbol = resolve(literalContext.name.getText()); - if (optSymbol.isPresent()) { - literalSymbols.add((XstsCustomLiteralSymbol) optSymbol.get()); - } else { - var symbol = new XstsCustomLiteralSymbol(literalContext.name.getText()); - literalSymbols.add(symbol); - declare(symbol); - env.define(symbol, symbol.instantiate()); - } - } - final List literals = literalSymbols.stream() - .map(XstsCustomLiteralSymbol::getLiteral).collect(Collectors.toList()); - final XstsCustomType xstsCustomType = XstsCustomType.of(typeDeclContext.name.getText(), - literals); - - final XstsCustomTypeSymbol typeDeclSymbol = XstsCustomTypeSymbol.of(xstsCustomType); + final String typeName = typeDeclContext.name.getText(); + final List literalNames = new ArrayList<>(); + typeDeclContext.literals.forEach(litCtx -> literalNames.add(litCtx.name.getText())); + customTypeShortNames.addAll(literalNames); + final EnumType enumType = EnumType.of(typeName, literalNames); + literalNames + .stream() + .map(litName -> EnumType.makeLongName(enumType, litName)) + .map(fullLitName -> XstsCustomLiteralSymbol.of(enumType, fullLitName)) + .forEach(symbol -> { + declare(symbol); + env.define(symbol, symbol.instantiate()); + }); + + final XstsCustomTypeSymbol typeDeclSymbol = XstsCustomTypeSymbol.of(enumType); typeTable.add(typeDeclSymbol); - env.define(typeDeclSymbol, typeDeclSymbol.getXstsType()); + env.define(typeDeclSymbol, enumType); } for (var varDeclContext : context.variableDeclarations) { - if (tempVarPattern.matcher(varDeclContext.name.getText()).matches()) { + final String varName = varDeclContext.name.getText(); + if (tempVarPattern.matcher(varName).matches()) { throw new ParseException(varDeclContext, - "Variable name '" + varDeclContext.name.getText() + "' is reserved!"); + "Variable name '" + varName + "' is reserved!"); } + if (customTypeShortNames.contains(varName)) + throw new ParseException(varDeclContext, + String.format("Variable name '%s' matches at least one declared enum literal", varName)); - final XstsVariableSymbol symbol = new XstsVariableSymbol(typeTable, varToType, - varDeclContext); + final XstsVariableSymbol symbol = new XstsVariableSymbol(typeTable, varDeclContext); declare(symbol); final VarDecl var = symbol.instantiate(env); @@ -107,29 +106,42 @@ public XSTS instantiate() { ctrlVars.add(var); } if (varDeclContext.initValue != null) { + var scope = new BasicDynamicScope(this); + if (var.getType() instanceof EnumType enumType) { + env.push(); + enumType.getValues().forEach(literal -> { + Symbol fullNameSymbol = resolve(EnumType.makeLongName(enumType, literal)).orElseThrow(); + if (fullNameSymbol instanceof XstsCustomLiteralSymbol fNameCustLitSymbol) { + var customSymbol = XstsCustomLiteralSymbol.copyWithName(fNameCustLitSymbol, literal); + scope.declare(customSymbol); + env.define(customSymbol, customSymbol.instantiate()); + } else { + throw new IllegalArgumentException(String.format("%s is not a literal of type %s", literal, enumType.getName())); + } + }); + } initExprs.add(Eq(var.getRef(), - new XstsExpression(this, typeTable, varDeclContext.initValue).instantiate( + new XstsExpression(scope, typeTable, varDeclContext.initValue).instantiate( env))); + if (var.getType() instanceof EnumType) + env.pop(); } env.define(symbol, var); } final NonDetStmt tranSet = new XstsTransitionSet(this, typeTable, - context.tran.transitionSet(), varToType).instantiate(env); + context.tran.transitionSet()).instantiate(env); final NonDetStmt initSet = new XstsTransitionSet(this, typeTable, - context.init.transitionSet(), varToType).instantiate(env); + context.init.transitionSet()).instantiate(env); final NonDetStmt envSet = new XstsTransitionSet(this, typeTable, - context.env.transitionSet(), varToType).instantiate(env); + context.env.transitionSet()).instantiate(env); - for (VarDecl varDecl : varToType.keySet()) { - initExprs.add(varToType.get(varDecl).createBoundExpr(varDecl)); - } final Expr initFormula = ExprUtils.simplify(And(initExprs)); final Expr prop = cast( new XstsExpression(this, typeTable, context.prop).instantiate(env), Bool()); - return new XSTS(varToType, ctrlVars, initSet, tranSet, envSet, initFormula, prop); + return new XSTS(ctrlVars, initSet, tranSet, envSet, initFormula, prop); } @Override diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java index c971c82c6c..74b235ec0f 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java @@ -15,31 +15,30 @@ */ package hu.bme.mit.theta.xsts.dsl; -import com.google.common.collect.ImmutableList; import hu.bme.mit.theta.common.dsl.*; import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.dsl.DeclSymbol; import hu.bme.mit.theta.core.dsl.ParseException; +import hu.bme.mit.theta.core.stmt.NonDetStmt; +import hu.bme.mit.theta.core.stmt.SequenceStmt; import hu.bme.mit.theta.core.stmt.*; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.enumtype.EnumType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; -import hu.bme.mit.theta.xsts.type.XstsCustomType; import java.util.ArrayList; import java.util.List; -import java.util.Map; import static com.google.common.base.Preconditions.*; import static hu.bme.mit.theta.core.stmt.Stmts.*; import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; @@ -48,19 +47,16 @@ public class XstsStatement { private final DynamicScope scope; private final SymbolTable typeTable; private final StmtContext context; - private final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType; public XstsStatement(final DynamicScope scope, final SymbolTable typeTable, - final StmtContext context, - final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType) { + final StmtContext context) { this.scope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.context = checkNotNull(context); - this.varToType = checkNotNull(varToType); } public Stmt instantiate(final Env env) { - final StmtCreatorVisitor visitor = new StmtCreatorVisitor(scope, typeTable, env, varToType); + final StmtCreatorVisitor visitor = new StmtCreatorVisitor(scope, typeTable, env); final Stmt stmt = context.accept(visitor); if (stmt == null) { throw new AssertionError(); @@ -73,16 +69,13 @@ private static final class StmtCreatorVisitor extends XstsDslBaseVisitor { private DynamicScope currentScope; private final SymbolTable typeTable; - final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType; private final Env env; public StmtCreatorVisitor(final DynamicScope scope, final SymbolTable typeTable, - final Env env, - final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType) { + final Env env) { this.currentScope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.env = checkNotNull(env); - this.varToType = checkNotNull(varToType); } private void push() { @@ -104,13 +97,6 @@ public Stmt visitHavocStmt(final HavocStmtContext ctx) { final Symbol lhsSymbol = currentScope.resolve(lhsId).get(); final VarDecl var = (VarDecl) env.eval(lhsSymbol); - final hu.bme.mit.theta.xsts.type.XstsType type = varToType.get(var); - if (type instanceof XstsCustomType) { - final Expr expr = type.createBoundExpr(var); - final AssumeStmt assume = Assume(expr); - return SequenceStmt.of(List.of(Havoc(var), assume)); - } - return Havoc(var); } @@ -128,10 +114,15 @@ public Stmt visitAssignStmt(final AssignStmtContext ctx) { final Symbol lhsSymbol = currentScope.resolve(lhsId).get(); final VarDecl var = (VarDecl) env.eval(lhsSymbol); + if (var.getType() instanceof EnumType enumType) { + env.push(); + enumType.getValues().forEach(literal -> CustomTypeDeclarationUtil.declareTypeWithShortName(currentScope, enumType, literal, env)); + } final XstsExpression expression = new XstsExpression(currentScope, typeTable, ctx.value); final Expr expr = expression.instantiate(env); - + if (var.getType() instanceof EnumType) + env.pop(); if (expr.getType().equals(var.getType())) { @SuppressWarnings("unchecked") final VarDecl tVar = (VarDecl) var; @SuppressWarnings("unchecked") final Expr tExpr = (Expr) expr; @@ -222,21 +213,14 @@ public Stmt visitLoopStmt(LoopStmtContext ctx) { @SuppressWarnings("unchecked") public Stmt visitLocalVarDeclStmt(LocalVarDeclStmtContext ctx) { final String name = ctx.name.getText(); - final hu.bme.mit.theta.xsts.type.XstsType xstsType = new XstsType(typeTable, + final Type type = new XstsType(typeTable, ctx.ttype).instantiate(env); - final Type type = xstsType.getType(); final var decl = Decls.Var(name, type); final Symbol symbol = DeclSymbol.of(decl); final Stmt result; if (ctx.initValue == null) { - if (xstsType instanceof XstsCustomType) { - final Expr expr = xstsType.createBoundExpr(decl); - final AssumeStmt assume = Assume(expr); - result = assume; - } else { - result = SkipStmt.getInstance(); - } + result = SkipStmt.getInstance(); } else { var expr = new XstsExpression(currentScope, typeTable, ctx.initValue).instantiate( env); @@ -252,7 +236,6 @@ public Stmt visitLocalVarDeclStmt(LocalVarDeclStmtContext ctx) { currentScope.declare(symbol); env.define(symbol, decl); - varToType.put(decl, xstsType); return result; } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java index f4bfefe7de..700f010355 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java @@ -17,18 +17,13 @@ import hu.bme.mit.theta.common.dsl.DynamicScope; import hu.bme.mit.theta.common.dsl.Env; -import hu.bme.mit.theta.common.dsl.Scope; import hu.bme.mit.theta.common.dsl.SymbolTable; -import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.NonDetStmt; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.TransitionSetContext; -import hu.bme.mit.theta.xsts.type.XstsType; import java.util.List; -import java.util.Map; -import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkNotNull; @@ -37,14 +32,12 @@ public class XstsTransitionSet { private final DynamicScope scope; private final SymbolTable typeTable; private final TransitionSetContext context; - private final Map, XstsType> varToType; public XstsTransitionSet(final DynamicScope scope, final SymbolTable typeTable, - final TransitionSetContext context, final Map, XstsType> varToType) { + final TransitionSetContext context) { this.scope = checkNotNull(scope); this.typeTable = checkNotNull(typeTable); this.context = checkNotNull(context); - this.varToType = checkNotNull(varToType); } public NonDetStmt instantiate(final Env env) { @@ -68,8 +61,9 @@ public TransitionSetCreatorVisitor(final Env env) { @Override public NonDetStmt visitTransitionSet(TransitionSetContext ctx) { final List stmts = ctx.stmts.stream() - .map((stmtContext -> new XstsStatement(scope, typeTable, stmtContext, - varToType).instantiate(env))).collect(Collectors.toList()); + .map((stmtContext -> + new XstsStatement(scope, typeTable, stmtContext) + .instantiate(env))).toList(); return NonDetStmt.of(stmts); } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsType.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsType.java index 172281a66d..7ded3def8b 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsType.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsType.java @@ -19,10 +19,9 @@ import hu.bme.mit.theta.common.dsl.Symbol; import hu.bme.mit.theta.common.dsl.SymbolTable; import hu.bme.mit.theta.core.dsl.ParseException; +import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*; -import hu.bme.mit.theta.xsts.type.XstsArrayType; -import hu.bme.mit.theta.xsts.type.XstsPrimitiveType; import java.util.Optional; @@ -41,9 +40,9 @@ public XstsType(final SymbolTable typeTable, final TypeContext context) { this.context = checkNotNull(context); } - public hu.bme.mit.theta.xsts.type.XstsType instantiate(final Env env) { + public Type instantiate(final Env env) { final TypeCreatorVisitor typeCreatorVisitor = new TypeCreatorVisitor(typeTable, env); - final hu.bme.mit.theta.xsts.type.XstsType result = context.accept(typeCreatorVisitor); + final Type result = context.accept(typeCreatorVisitor); if (result == null) { throw new AssertionError(); } else { @@ -52,7 +51,7 @@ public hu.bme.mit.theta.xsts.type.XstsType instantiate(final Env env) { } private static class TypeCreatorVisitor extends - XstsDslBaseVisitor { + XstsDslBaseVisitor { private final SymbolTable typeTable; private final Env env; @@ -63,33 +62,31 @@ public TypeCreatorVisitor(final SymbolTable typeTable, final Env env) { } @Override - public hu.bme.mit.theta.xsts.type.XstsType visitCustomType(final CustomTypeContext ctx) { + public Type visitCustomType(final CustomTypeContext ctx) { Optional optSymbol = typeTable.get(ctx.name.getText()); if (optSymbol.isEmpty()) { throw new ParseException(ctx, "Type '" + ctx.name.getText() + "' cannot be resolved"); } final Symbol symbol = optSymbol.get(); - final hu.bme.mit.theta.xsts.type.XstsType xstsType = (hu.bme.mit.theta.xsts.type.XstsType) env.eval( - symbol); - return xstsType; + return (Type) env.eval(symbol); } @Override - public hu.bme.mit.theta.xsts.type.XstsType visitBoolType(final BoolTypeContext ctx) { - return XstsPrimitiveType.of(Bool()); + public Type visitBoolType(final BoolTypeContext ctx) { + return Bool(); } @Override - public hu.bme.mit.theta.xsts.type.XstsType visitIntType(final IntTypeContext ctx) { - return XstsPrimitiveType.of(Int()); + public Type visitIntType(final IntTypeContext ctx) { + return Int(); } @Override - public hu.bme.mit.theta.xsts.type.XstsType visitArrayType(final ArrayTypeContext ctx) { - final hu.bme.mit.theta.xsts.type.XstsType indexType = ctx.indexType.accept(this); - final hu.bme.mit.theta.xsts.type.XstsType elemType = ctx.elemType.accept(this); - return XstsArrayType.of(indexType, elemType); + public Type visitArrayType(final ArrayTypeContext ctx) { + final Type indexType = ctx.indexType.accept(this); + final Type elemType = ctx.elemType.accept(this); + return Array(indexType, elemType); } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsVariableSymbol.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsVariableSymbol.java index 4ec5d2c875..f0727ce176 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsVariableSymbol.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsVariableSymbol.java @@ -21,8 +21,6 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.VariableDeclarationContext; -import java.util.Map; - import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.decl.Decls.Var; @@ -30,14 +28,11 @@ public class XstsVariableSymbol implements Symbol { private final String name; private final XstsType type; - final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType; public XstsVariableSymbol(final SymbolTable typeTable, - final Map, hu.bme.mit.theta.xsts.type.XstsType> varToType, final VariableDeclarationContext context) { checkNotNull(context); name = context.name.getText(); - this.varToType = varToType; type = new XstsType(typeTable, context.ttype); } @@ -47,9 +42,6 @@ public String getName() { } public VarDecl instantiate(Env env) { - final hu.bme.mit.theta.xsts.type.XstsType xstsType = type.instantiate(env); - final VarDecl var = Var(name, xstsType.getType()); - varToType.put(var, xstsType); - return var; + return Var(name, type.instantiate(env)); } } diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java index 49e15dc922..c0fd04df59 100644 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java +++ b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/pnml/PnmlToXSTS.java @@ -16,7 +16,6 @@ package hu.bme.mit.theta.xsts.pnml; import com.google.common.collect.ImmutableList; -import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; import hu.bme.mit.theta.common.container.Containers; import hu.bme.mit.theta.core.decl.Decls; @@ -29,7 +28,6 @@ import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.xsts.XSTS; import hu.bme.mit.theta.xsts.pnml.elements.*; -import hu.bme.mit.theta.xsts.type.XstsType; import java.io.InputStream; import java.util.*; @@ -104,8 +102,6 @@ public static XSTS createXSTS(final PnmlNet net, final InputStream propStream) { final NonDetStmt tran = NonDetStmt.of(tranStmts); final NonDetStmt init = NonDetStmt.of(ImmutableList.of()); final NonDetStmt env = NonDetStmt.of(ImmutableList.of()); - - final Map, XstsType> varToType = ImmutableMap.of(); final Set> ctrlVars = ImmutableSet.of(); final Scanner propScanner = new Scanner(propStream).useDelimiter("\\A"); @@ -136,7 +132,7 @@ public static XSTS createXSTS(final PnmlNet net, final InputStream propStream) { propExpr = cast(dslManager.parseExpr(property), Bool()); } - return new XSTS(varToType, ctrlVars, init, tran, env, initExpr, propExpr); + return new XSTS(ctrlVars, init, tran, env, initExpr, propExpr); } private static String stripPropFromPropFile(final String propertyFile) { diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsArrayType.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsArrayType.java deleted file mode 100644 index dcc1a3e605..0000000000 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsArrayType.java +++ /dev/null @@ -1,70 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xsts.type; - -import com.google.common.base.Preconditions; -import hu.bme.mit.theta.common.Utils; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; -import hu.bme.mit.theta.core.type.arraytype.ArrayType; -import hu.bme.mit.theta.core.type.booltype.BoolType; - -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - -public final class XstsArrayType implements - XstsType> { - - private final XstsType indexType; - private final XstsType elemType; - private ArrayType type; - - private XstsArrayType(XstsType indexType, XstsType elemType) { - this.indexType = indexType; - this.elemType = elemType; - this.type = Array(indexType.getType(), elemType.getType()); - } - - public static XstsArrayType of( - XstsType indexType, XstsType elemType) { - return new XstsArrayType<>(indexType, elemType); - } - - public ArrayType getType() { - return type; - } - - @Override - public Expr createBoundExpr(VarDecl> decl) { - return True(); - } - - @Override - public String serializeLiteral(LitExpr> literal) { - Preconditions.checkArgument(literal.getType().equals(type)); - final ArrayLitExpr arrayLitExpr = (ArrayLitExpr) literal; - return Utils.lispStringBuilder("array") - .addAll(arrayLitExpr.getElements().stream().map( - elem -> String.format("(%s %s)", indexType.serializeLiteral(elem.get1()), - elemType.serializeLiteral(elem.get2())))) - .add((String.format("(default %s)", - elemType.serializeLiteral(arrayLitExpr.getElseElem())))) - .toString(); - } -} diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsCustomType.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsCustomType.java deleted file mode 100644 index 3d9f404d1e..0000000000 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsCustomType.java +++ /dev/null @@ -1,99 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xsts.type; - -import com.google.common.base.Preconditions; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.inttype.IntLitExpr; -import hu.bme.mit.theta.core.type.inttype.IntType; - -import java.math.BigInteger; -import java.util.List; -import java.util.stream.Collectors; - -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; -import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; - -public final class XstsCustomType implements XstsType { - - private final String name; - private final List literals; - - private XstsCustomType(final String name, final List literals) { - this.name = name; - this.literals = literals; - } - - public static XstsCustomType of(final String name, final List literals) { - return new XstsCustomType(name, literals); - } - - public String getName() { - return name; - } - - public List getLiterals() { - return literals; - } - - public static final class XstsCustomLiteral { - - private final BigInteger intValue; - private final String name; - - private XstsCustomLiteral(String name, BigInteger intValue) { - this.name = name; - this.intValue = intValue; - } - - public static XstsCustomLiteral of(String name, BigInteger intValue) { - return new XstsCustomLiteral(name, intValue); - } - - public BigInteger getIntValue() { - return intValue; - } - - public String getName() { - return name; - } - } - - public IntType getType() { - return Int(); - } - - @Override - public Expr createBoundExpr(VarDecl decl) { - return Or(literals.stream() - .map(lit -> Eq(decl.getRef(), Int(lit.getIntValue()))) - .collect(Collectors.toList())); - } - - @Override - public String serializeLiteral(LitExpr literal) { - final IntLitExpr intLitExpr = (IntLitExpr) literal; - final var customLiteral = literals.stream() - .filter(lit -> lit.getIntValue().equals(intLitExpr.getValue())).findFirst(); - Preconditions.checkArgument(customLiteral.isPresent(), "Literal %s not found", - intLitExpr.getValue()); - return customLiteral.get().getName(); - } -} diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsPrimitiveType.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsPrimitiveType.java deleted file mode 100644 index c353874c52..0000000000 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsPrimitiveType.java +++ /dev/null @@ -1,54 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.xsts.type; - -import com.google.common.base.Preconditions; -import hu.bme.mit.theta.core.decl.VarDecl; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.LitExpr; -import hu.bme.mit.theta.core.type.Type; -import hu.bme.mit.theta.core.type.booltype.BoolType; - -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; - -public final class XstsPrimitiveType implements XstsType { - - private final T type; - - private XstsPrimitiveType(T type) { - this.type = type; - } - - public static XstsPrimitiveType of(T type) { - return new XstsPrimitiveType<>(type); - } - - @Override - public T getType() { - return type; - } - - @Override - public Expr createBoundExpr(VarDecl decl) { - return True(); - } - - @Override - public String serializeLiteral(LitExpr literal) { - Preconditions.checkArgument(literal.getType().equals(type)); - return literal.toString(); - } -} diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ChanType.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ChanType.java index ded9bc6e4c..8ccf501c22 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ChanType.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ChanType.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xta.utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Type; public final class ChanType implements Type { @@ -33,4 +34,8 @@ public String toString() { return "Chan"; } + @Override + public DomainSize getDomainSize() { + return DomainSize.ONE; + } } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ClockType.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ClockType.java index dc3c18a036..cf7cb2fb63 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ClockType.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/ClockType.java @@ -15,6 +15,7 @@ */ package hu.bme.mit.theta.xta.utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Type; public final class ClockType implements Type { @@ -33,4 +34,8 @@ public String toString() { return "Clock"; } + @Override + public DomainSize getDomainSize() { + return DomainSize.INFINITY; + } } diff --git a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/RangeType.java b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/RangeType.java index 7e983d43bd..8fd2a66254 100644 --- a/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/RangeType.java +++ b/subprojects/xta/xta/src/main/java/hu/bme/mit/theta/xta/utils/RangeType.java @@ -15,16 +15,17 @@ */ package hu.bme.mit.theta.xta.utils; -import static com.google.common.base.Preconditions.checkArgument; - -import java.util.stream.IntStream; -import java.util.stream.Stream; - import hu.bme.mit.theta.common.Utils; +import hu.bme.mit.theta.core.type.DomainSize; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.inttype.IntExprs; import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import java.util.stream.IntStream; +import java.util.stream.Stream; + +import static com.google.common.base.Preconditions.checkArgument; + public final class RangeType implements Type { private static final int HASH_SEED = 5441; @@ -89,4 +90,9 @@ public String toString() { return Utils.lispStringBuilder("Range").add(lower).add(upper).toString(); } + @Override + public DomainSize getDomainSize() { + return DomainSize.of(upper - lower + 1); + } + }