Enumtype smtlib

build.gradle.kts

@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "5.2.1"
+    version = "5.3.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

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

@@ -0,0 +1,100 @@
+/*
+ *  Copyright 2024 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 {
+
+    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 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));
+    }
+
+    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 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));
+    }
+
+    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;
+    }
+
+    @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

@@ -16,6 +16,7 @@
 package hu.bme.mit.theta.core.type.arraytype;
 
 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;
@@ -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,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<BvType> Geq(Expr<BvType> leftOp, Expr<BvType> rightOp) {
             return BvExprs.UGeq(leftOp, rightOp);
         }
     }
+
+    @Override
+    public DomainSize getDomainSize() {
+        return DomainSize.of(BigInteger.TWO.pow(size));
+    }
 }

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

@@ -0,0 +1,78 @@
+/*
+ *  Copyright 2024 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,82 @@
+/*
+ *  Copyright 2024 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 = EnumType.getShortName(literalName);
+        checkArgument(type.getValues().contains(value), "Invalid value %s for type %s", value, type.getName());
+        return new EnumLitExpr(type, value);
+    }
+
+    public static BoolLitExpr eq(EnumLitExpr l, EnumLitExpr r) {
+        return Bool(l.type.equals(r.type) && l.value.equals(r.value));
+    }
+
+    public static BoolLitExpr neq(EnumLitExpr l, EnumLitExpr r) {
+        return Bool(!l.type.equals(r.type) || !l.value.equals(r.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);
+    }
+
+    @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);
+    }
+}