Merge pull request #134 from ftsrg/xsts-arrayinit

Added ArrayInitExprs to XSTS
ftsrg · Aug 11, 2021 · e10eede · e10eede
2 parents 9e0cc97 + ebdd6cd
commit e10eede
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 7 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.21.0"
+    version = "2.22.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

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
@@ -51,9 +51,7 @@
 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.arraytype.ArrayExprs.Array;
-import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read;
-import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write;
+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;
@@ -64,6 +62,7 @@
 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.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;
@@ -506,7 +505,7 @@ private <T1 extends Type, T2 extends Type> Expr<?> createArrayLitExpr(final ArrL
 			}
 			valueType = (T2) ctx.elseExpr.accept(this).getType();
 
-			final List<Tuple2<? extends Expr<T1>, ? extends Expr<T2>>> elems = IntStream
+			final List<Tuple2<Expr<T1>,Expr<T2>>> elems = IntStream
 					.range(0, ctx.indexExpr.size())
 					.mapToObj(i -> Tuple2.of(
 							cast(ctx.indexExpr.get(i).accept(this), indexType),
@@ -515,8 +514,7 @@ private <T1 extends Type, T2 extends Type> Expr<?> createArrayLitExpr(final ArrL
 					.collect(Collectors.toUnmodifiableList());
 
 			final Expr<T2> elseExpr = cast(ctx.elseExpr.accept(this), valueType);
-			return Array(elems, elseExpr, ArrayType.of(indexType, valueType));
-		}
+			return simplify(ArrayInit(elems, elseExpr, ArrayType.of(indexType, valueType)));		}
 
 		@Override
 		public Expr<?> visitIdExpr(final IdExprContext ctx) {