Remove xsts type layer from above native types

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

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<VarDecl<?>> vars;
-    private final Map<VarDecl<?>, XstsType<?>> varToType;
     private final Set<VarDecl<?>> ctrlVars;
 
     private final NonDetStmt tran;
@@ -49,10 +49,6 @@ public Collection<VarDecl<?>> getVars() {
         return vars;
     }
 
-    public Map<VarDecl<?>, XstsType<?>> getVarToType() {
-        return varToType;
-    }
-
     public Expr<BoolType> getProp() {
         return prop;
     }
@@ -73,19 +69,17 @@ public Set<VarDecl<?>> getCtrlVars() {
         return ctrlVars;
     }
 
-    public XSTS(final Map<VarDecl<?>, XstsType<?>> varToType, final Set<VarDecl<?>> ctrlVars,
+    public XSTS(final Set<VarDecl<?>> ctrlVars,
                 final NonDetStmt init, final NonDetStmt tran, final NonDetStmt env,
                 final Expr<BoolType> initFormula, final Expr<BoolType> prop) {
         this.tran = checkNotNull(tran);
         this.init = checkNotNull(init);
         this.env = checkNotNull(env);
         this.initFormula = checkNotNull(initFormula);
         this.prop = checkNotNull(prop);
-        this.varToType = varToType;
         this.ctrlVars = ctrlVars;
 
         final Set<VarDecl<?>> tmpVars = Containers.createSet();
-        tmpVars.addAll(varToType.keySet());
         tmpVars.addAll(StmtUtils.getVars(tran));
         tmpVars.addAll(StmtUtils.getVars(env));
         tmpVars.addAll(StmtUtils.getVars(init));

subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java

@@ -478,7 +478,7 @@ private <T1 extends Type, T2 extends Type> 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();
             }

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<? extends Symbol> resolve(String name) {
     public XSTS instantiate() {
         final Env env = new Env();
 
-        final Map<VarDecl<?>, XstsType<?>> varToType = Containers.createMap();
         final Set<VarDecl<?>> ctrlVars = Containers.createSet();
         final List<Expr<BoolType>> 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<BoolType> initFormula = ExprUtils.simplify(And(initExprs));
 
         final Expr<BoolType> 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

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<VarDecl<?>, hu.bme.mit.theta.xsts.type.XstsType<?>> varToType;
 
     public XstsStatement(final DynamicScope scope, final SymbolTable typeTable,
-                         final StmtContext context,
-                         final Map<VarDecl<?>, 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<Stmt> {
 
         private DynamicScope currentScope;
         private final SymbolTable typeTable;
-        final Map<VarDecl<?>, 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<VarDecl<?>, 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<BoolType> 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<BoolType> 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;
         }

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<VarDecl<?>, XstsType<?>> varToType;
 
     public XstsTransitionSet(final DynamicScope scope, final SymbolTable typeTable,
-                             final TransitionSetContext context, final Map<VarDecl<?>, 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<Stmt> 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);
         }
     }

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<hu.bme.mit.theta.xsts.type.XstsType> {
+            XstsDslBaseVisitor<Type> {
 
         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<? extends Symbol> 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);
         }
 
     }