EnumType and DomainSize

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/DomainSize.java

@@ -0,0 +1,98 @@
+/*
+ *  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;
+
+public class DomainSize {
+
+	private final BigInteger finiteSize;
+
+	private DomainSize(BigInteger value) {
+		finiteSize = value;
+	}
+
+	public static DomainSize of(BigInteger val) {
+		return new DomainSize(val);
+	}
+
+	public static DomainSize of(long val) {
+		return of(BigInteger.valueOf(val));
+	}
+
+	public static final DomainSize INFINITY = of(-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<BigInteger> 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 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);
+	}
+}

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();
 }

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<IndexType extends Type, ElemType extends Type>
         implements Equational<ArrayType<IndexType, ElemType>> {
 
@@ -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());
+    }
 }

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<BoolType> Neq(final Expr<BoolType> leftOp, final Expr<BoolType> r
         return BoolExprs.Xor(leftOp, rightOp);
     }
 
+    @Override
+    public DomainSize getDomainSize() {
+        return DomainSize.TWO;
+    }
+
 }

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java

@@ -17,28 +17,10 @@
 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;
 
@@ -223,4 +205,9 @@ public GeqExpr<BvType> Geq(Expr<BvType> leftOp, Expr<BvType> rightOp) {
             return BvExprs.UGeq(leftOp, rightOp);
         }
     }
+
+    @Override
+    public DomainSize getDomainSize() {
+        return DomainSize.of((long) Math.pow(2, size));
+    }
 }

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<EnumType> {
+
+	private static final int HASH_SEED = 5326;
+	private static final String OPERATOR_LABEL = "=";
+
+	private EnumEqExpr(Expr<EnumType> leftOp, Expr<EnumType> rightOp) {
+		super(leftOp, rightOp);
+	}
+
+	public static EnumEqExpr of(Expr<EnumType> leftOp, Expr<EnumType> rightOp) {
+		return new EnumEqExpr(leftOp, rightOp);
+	}
+
+	@Override
+	public BinaryExpr<EnumType, BoolType> with(Expr<EnumType> leftOp, Expr<EnumType> rightOp) {
+		if (leftOp == getLeftOp() && rightOp == getRightOp()) {
+			return this;
+		} else {
+			return EnumEqExpr.of(leftOp, rightOp);
+		}
+	}
+
+	@Override
+	public BinaryExpr<EnumType, BoolType> withLeftOp(Expr<EnumType> leftOp) {
+		return with(leftOp, getRightOp());
+	}
+
+	@Override
+	public BinaryExpr<EnumType, BoolType> withRightOp(Expr<EnumType> 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<BoolType> eval(Valuation val) {
+		return EnumLitExpr.eq((EnumLitExpr) getLeftOp().eval(val), (EnumLitExpr) getRightOp().eval(val));
+	}
+}

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<EnumType> implements LitExpr<EnumType> {
+
+	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 = literalName.contains(".") ? literalName.substring(literalName.indexOf(".") + 1) : 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<EnumType> 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);
+	}
+}