-
Notifications
You must be signed in to change notification settings - Fork 43
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #272 from RipplB/enumtype_smtlib
Enumtype smtlib
- Loading branch information
Showing
80 changed files
with
1,813 additions
and
1,615 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
100 changes: 100 additions & 0 deletions
100
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/DomainSize.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -16,5 +16,5 @@ | |
| package hu.bme.mit.theta.core.type; | ||
|
|
||
| public interface Type { | ||
|
|
||
| DomainSize getDomainSize(); | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
78 changes: 78 additions & 0 deletions
78
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumEqExpr.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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)); | ||
| } | ||
| } |
82 changes: 82 additions & 0 deletions
82
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumLitExpr.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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); | ||
| } | ||
| } |
Oops, something went wrong.