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/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/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java index 86de4b8fe0..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 @@ -478,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(); } 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 e1c699665e..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 @@ -26,8 +26,6 @@ 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; @@ -67,7 +65,6 @@ 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<>(); @@ -88,7 +85,7 @@ public XSTS instantiate() { final XstsCustomTypeSymbol typeDeclSymbol = XstsCustomTypeSymbol.of(enumType); typeTable.add(typeDeclSymbol); - env.define(typeDeclSymbol, XstsCustomType.of(enumType)); + env.define(typeDeclSymbol, enumType); } for (var varDeclContext : context.variableDeclarations) { @@ -101,8 +98,7 @@ public XSTS instantiate() { 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); @@ -114,7 +110,7 @@ public XSTS instantiate() { if (var.getType() instanceof EnumType enumType) { env.push(); enumType.getValues().forEach(literal -> { - Symbol fullNameSymbol = resolve(String.format("%s%s%s", enumType.getName(), EnumType.FULLY_QUALIFIED_NAME_SEPARATOR, literal)).orElseThrow(); + Symbol fullNameSymbol = resolve(EnumType.makeLongName(enumType, literal)).orElseThrow(); if (fullNameSymbol instanceof XstsCustomLiteralSymbol fNameCustLitSymbol) { var customSymbol = XstsCustomLiteralSymbol.copyWithName(fNameCustLitSymbol, literal); scope.declare(customSymbol); @@ -134,21 +130,18 @@ public XSTS instantiate() { } 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 85488d44bb..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 @@ -31,11 +31,9 @@ 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.*; @@ -49,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(); @@ -74,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() { @@ -105,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); } @@ -228,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); @@ -258,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 8d757b6537..0000000000 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsCustomType.java +++ /dev/null @@ -1,60 +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 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.enumtype.EnumLitExpr; -import hu.bme.mit.theta.core.type.enumtype.EnumType; - -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; - -public final class XstsCustomType implements XstsType { - - private final EnumType type; - - private XstsCustomType(EnumType type) { - this.type = type; - } - - public static XstsCustomType of(EnumType type) { - return new XstsCustomType(type); - } - - public String getName() { - return type.getName(); - } - - @Override - public EnumType getType() { - return type; - } - - @Override - public Expr createBoundExpr(VarDecl decl) { - return Or(type.getValues().stream() - .map(lit -> Eq(decl.getRef(), EnumLitExpr.of(type, lit))) - .toList()); - } - - @Override - public String serializeLiteral(LitExpr literal) { - return literal.toString(); - } -} 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/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java deleted file mode 100644 index 1d40f9a9b5..0000000000 --- a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/type/XstsType.java +++ /dev/null @@ -1,32 +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 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; - -public interface XstsType { - - T getType(); - - Expr createBoundExpr(final VarDecl decl); - - String serializeLiteral(final LitExpr literal); - -}