From 379b0c30e80d6a8a68da9fe0b50c5bf860985b2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hajdu=20=C3=81kos?= <hajdua@mit.bme.hu>
Date: Tue, 30 Jun 2020 17:02:43 +0200
Subject: [PATCH] Improve documentation for expressions

---
 subprojects/core/README.md                    |  9 ++++--
 .../mit/theta/core/decl/BasicConstDecl.java   |  4 +++
 .../hu/bme/mit/theta/core/decl/ConstDecl.java |  6 ++++
 .../hu/bme/mit/theta/core/decl/Decls.java     | 24 ++++++++++++++++
 .../mit/theta/core/decl/IndexedConstDecl.java |  6 ++++
 .../hu/bme/mit/theta/core/decl/VarDecl.java   |  6 ++++
 .../bme/mit/theta/core/decl/package-info.java | 10 +++++--
 .../mit/theta/core/model/Substitution.java    | 13 +++++++--
 .../bme/mit/theta/core/model/Valuation.java   | 15 ++++++++--
 .../mit/theta/core/model/package-info.java    | 13 +++++----
 .../bme/mit/theta/core/stmt/AssignStmt.java   |  5 ++++
 .../bme/mit/theta/core/stmt/AssumeStmt.java   |  4 +++
 .../hu/bme/mit/theta/core/stmt/HavocStmt.java |  5 ++++
 .../hu/bme/mit/theta/core/stmt/SkipStmt.java  |  3 ++
 .../hu/bme/mit/theta/core/stmt/Stmts.java     |  5 ++++
 .../bme/mit/theta/core/stmt/package-info.java |  6 ++--
 .../core/type/abstracttype/package-info.java  | 24 ++++++++++++++++
 .../theta/core/type/anytype/package-info.java |  9 ++++++
 .../core/type/arraytype/package-info.java     | 17 +++++++++++
 .../core/type/booltype/package-info.java      | 20 +++++++++++++
 .../theta/core/type/inttype/package-info.java | 28 +++++++++++++++++++
 .../bme/mit/theta/core/type/package-info.java | 18 ++++++------
 .../theta/core/type/rattype/package-info.java | 22 +++++++++++++++
 23 files changed, 246 insertions(+), 26 deletions(-)
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/package-info.java
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/anytype/package-info.java
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/package-info.java
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/package-info.java
 create mode 100644 subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/package-info.java

diff --git a/subprojects/core/README.md b/subprojects/core/README.md
index 12a4211098..5dca2872c2 100644
--- a/subprojects/core/README.md
+++ b/subprojects/core/README.md
@@ -1,10 +1,15 @@
 This project provides classes and utilities to build and manipulate first order logic (FOL) expressions and related concepts, which serve as a basis for the formalisms and analyses.
 
 Classes include
-* types (e.g., int, bool),
+* types (e.g., Boolean, integer, rational, array),
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/type/package-info.java) for more details,
 * declarations (e.g., constants, variables),
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/decl/package-info.java) for more details,
 * expressions (e.g., logical connectives, arithmetic operations),
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/type/package-info.java) for more details,
 * models (e.g., assignments, valuations),
-* statements (e.g., assign, ifelse, while).
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/model/package-info.java) for more details,
+* statements (e.g., assign, assume, havoc),
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/stmt/package-info.java) for more details.
 
 Utilities include folding, unfolding, collecting atoms, collecting variables, etc.
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/BasicConstDecl.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/BasicConstDecl.java
index 8592dab962..e744861066 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/BasicConstDecl.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/BasicConstDecl.java
@@ -17,6 +17,10 @@
 
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * A basic constant declaration that can be directly passed to the SMT solver.
+ * @param <DeclType>
+ */
 public final class BasicConstDecl<DeclType extends Type> extends ConstDecl<DeclType> {
 
 	BasicConstDecl(final String name, final DeclType type) {
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/ConstDecl.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/ConstDecl.java
index a7b73f27db..9f587bc625 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/ConstDecl.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/ConstDecl.java
@@ -18,6 +18,12 @@
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Abstract base class for constants. Use {@link BasicConstDecl} for a basic
+ * constant, or {@link IndexedConstDecl} if the constant belongs to a variable
+ * for some index (e.g., during unfolding paths).
+ * @param <DeclType>
+ */
 public abstract class ConstDecl<DeclType extends Type> extends Decl<DeclType> {
 	private static final String DECL_LABEL = "Const";
 
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/Decls.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/Decls.java
index aad621f562..a00d91549a 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/Decls.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/Decls.java
@@ -17,19 +17,43 @@
 
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Factory class to create declarations.
+ */
 public final class Decls {
 
 	private Decls() {
 	}
 
+	/**
+	 * Create a constant declaration with a given name and type.
+	 * @param name
+	 * @param type
+	 * @param <T>
+	 * @return
+	 */
 	public static <T extends Type> ConstDecl<T> Const(final String name, final T type) {
 		return new BasicConstDecl<>(name, type);
 	}
 
+	/**
+	 * Create a parameter declaration with a given name and type.
+	 * @param name
+	 * @param type
+	 * @param <T>
+	 * @return
+	 */
 	public static <T extends Type> ParamDecl<T> Param(final String name, final T type) {
 		return new ParamDecl<>(name, type);
 	}
 
+	/**
+	 * Create a variable declaration with a given type.
+	 * @param name
+	 * @param type
+	 * @param <T>
+	 * @return
+	 */
 	public static <T extends Type> VarDecl<T> Var(final String name, final T type) {
 		return new VarDecl<>(name, type);
 	}
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/IndexedConstDecl.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/IndexedConstDecl.java
index 738a4a4abb..98bc43ccc2 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/IndexedConstDecl.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/IndexedConstDecl.java
@@ -19,6 +19,12 @@
 
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * A constant declaration that belongs to a variable ({@link VarDecl} declaration
+ * for a given index. For example, when unfolding a path, each variable will have
+ * a new constant for each step of the path.
+ * @param <DeclType>
+ */
 public final class IndexedConstDecl<DeclType extends Type> extends ConstDecl<DeclType> {
 	private static final String NAME_FORMAT = "_%s:%d";
 
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java
index 540da7c93a..04b17e1094 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/VarDecl.java
@@ -23,6 +23,12 @@
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Represents a variable declaration. Variables cannot be directly passed to the SMT solver,
+ * they must be replaced with constants for a given index ({@link IndexedConstDecl}).
+ * See also {@link hu.bme.mit.theta.core.utils.PathUtils}.
+ * @param <DeclType>
+ */
 public final class VarDecl<DeclType extends Type> extends Decl<DeclType> {
 	private static final String DECL_LABEL = "var";
 
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/package-info.java
index 300988b289..c85e2bd757 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/package-info.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/decl/package-info.java
@@ -1,8 +1,12 @@
 /**
- * This package contains the different declarations (e.g., variables,
- * constants). Use the factory class to instantiate them.
+ * This package contains the different declarations.
+ * - {@link hu.bme.mit.theta.core.decl.ConstDecl} represents a constant that can be directly
+ *   handled by the SMT solvers.
+ * - {@link hu.bme.mit.theta.core.decl.VarDecl} represents a variable, that can have multiple
+ *   associated {@link hu.bme.mit.theta.core.decl.ConstDecl}s for each index (e.g. in a path)
+ * - {@link hu.bme.mit.theta.core.decl.ParamDecl} represents a parameter declaration.
  *
- * @see hu.bme.mit.theta.core.decl.Decls
+ * Use the factory class {@link hu.bme.mit.theta.core.decl.Decls} to instantiate them.
  */
 
 package hu.bme.mit.theta.core.decl;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Substitution.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Substitution.java
index b8a213b0c5..ec5584cb1e 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Substitution.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Substitution.java
@@ -24,13 +24,22 @@
 import hu.bme.mit.theta.core.type.anytype.RefExpr;
 
 /**
- * Interface for a substitution, which is a mapping from declarations to
- * expressions.
+ * Interface for a substitution, which is a mapping from declarations to expressions.
  */
 public interface Substitution {
 
+	/**
+	 * Get all the declarations for which an expression is assigned.
+	 * @return
+	 */
 	Collection<? extends Decl<?>> getDecls();
 
+	/**
+	 * Evaluate a declaration, i.e., get the corresponding expression.
+	 * @param decl
+	 * @param <DeclType>
+	 * @return
+	 */
 	<DeclType extends Type> Optional<? extends Expr<DeclType>> eval(final Decl<DeclType> decl);
 
 	default <T extends Type> Expr<T> apply(final Expr<T> expr) {
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Valuation.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Valuation.java
index 4224e452cb..dc7e05d7a6 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Valuation.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/Valuation.java
@@ -31,8 +31,7 @@
 import hu.bme.mit.theta.core.type.booltype.SmartBoolExprs;
 
 /**
- * Interface for a valuation, which is a mapping from declarations to literal
- * expressions.
+ * Interface for a valuation, which is a mapping from declarations to literal expressions.
  */
 public abstract class Valuation implements Substitution {
 	private static final int HASH_SEED = 2141;
@@ -42,6 +41,11 @@ public abstract class Valuation implements Substitution {
 
 	public abstract Map<Decl<?>, LitExpr<?>> toMap();
 
+	/**
+	 * Convert a valuation into an expression. For example if the valuation assigns
+	 * 1 to x and 2 to y, the expression is (x == 1 and y == 2).
+	 * @return
+	 */
 	public Expr<BoolType> toExpr() {
 		final List<Expr<BoolType>> exprs = new ArrayList<>();
 		for (final Decl<?> decl : getDecls()) {
@@ -51,6 +55,13 @@ public Expr<BoolType> toExpr() {
 		return SmartBoolExprs.And(exprs);
 	}
 
+	/**
+	 * Checks if an other valuation is more general than the current one. This holds
+	 * if the other valuation has the same or less declarations, and for each declaration,
+	 * the assigned value is the same.
+	 * @param that
+	 * @return
+	 */
 	public boolean isLeq(final Valuation that) {
 		if (that.getDecls().size() > this.getDecls().size()) {
 			return false;
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/package-info.java
index d1d4b2a72b..2bdb02d9f8 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/package-info.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/model/package-info.java
@@ -1,9 +1,12 @@
 /**
- * This package contains different implementations of models that assign
- * expressions or literals to declarations.
- *
- * @see hu.bme.mit.theta.core.model.Substitution
- * @see hu.bme.mit.theta.core.model.Valuation
+ * This package contains different implementations of models that assign expressions or literals to declarations.
+ * - {@link hu.bme.mit.theta.core.model.Substitution} is a substitution that maps expressions to declarations.
+ *   - {@link hu.bme.mit.theta.core.model.BasicSubstitution} is a basic implementation of a substitution.
+ *   - {@link hu.bme.mit.theta.core.model.NestedSubstitution} implements a scoped substitution.
+ * - {@link hu.bme.mit.theta.core.model.Valuation} is a special case of {@link hu.bme.mit.theta.core.model.Substitution}
+ *   where literal expressions are assigned to declarations.
+ *   - {@link hu.bme.mit.theta.core.model.MutableValuation} implements a mutable valuation.
+ *   - {@link hu.bme.mit.theta.core.model.ImmutableValuation} implements an immutable valuation.
  */
 
 package hu.bme.mit.theta.core.model;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssignStmt.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssignStmt.java
index 7b49f381e7..9a3623e182 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssignStmt.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssignStmt.java
@@ -23,6 +23,11 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Assignment statement of the form VARIABLE := EXPRESSION.
+ * The statement updates the VARIABLE with the result of EXPRESSION.
+ * @param <DeclType>
+ */
 public final class AssignStmt<DeclType extends Type> implements Stmt {
 
 	private static final int HASH_SEED = 409;
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssumeStmt.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssumeStmt.java
index 24042d2f47..0ce0d873e9 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssumeStmt.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/AssumeStmt.java
@@ -23,6 +23,10 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 
+/**
+ * Assume statement of the form [EXPRESSION], where EXPRESSION is a Boolean {@link Expr}.
+ * The statement is a guard that can only be passed if EXPRESSION evaluates to true.
+ */
 public final class AssumeStmt implements Stmt {
 
 	private static final int HASH_SEED = 547;
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/HavocStmt.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/HavocStmt.java
index c1979f943d..3632951c70 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/HavocStmt.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/HavocStmt.java
@@ -21,6 +21,11 @@
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Havoc statement of the form havoc VARIABLE, which performs a non-deterministic
+ * assignment to VARIABLE.
+ * @param <DeclType>
+ */
 public final class HavocStmt<DeclType extends Type> implements Stmt {
 
 	private static final int HASH_SEED = 929;
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/SkipStmt.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/SkipStmt.java
index 1d0c2b32dd..f6c1d5fe94 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/SkipStmt.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/SkipStmt.java
@@ -15,6 +15,9 @@
  */
 package hu.bme.mit.theta.core.stmt;
 
+/**
+ * A skip statement is a placeholder that does not perform any operation.
+ */
 public final class SkipStmt implements Stmt {
 
 	private static final int HASH_CODE = 1310147;
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java
index 26e572f588..7587d8c321 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/Stmts.java
@@ -20,6 +20,11 @@
 import hu.bme.mit.theta.core.type.Type;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 
+/**
+ * Factory class to instantiate different statements.
+ *
+ * @see Stmt
+ */
 public final class Stmts {
 
 	private Stmts() {
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/package-info.java
index 66304c8a1c..8e76b3ba74 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/package-info.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/stmt/package-info.java
@@ -1,9 +1,7 @@
 /**
  * This package contains statements (e.g., assignment, assume). Constructors of
- * the statements are usually package private, use the factory class to
- * instantiate them.
- *
- * @see hu.bme.mit.theta.core.stmt.Stmts
+ * the statements are usually package private, use the factory class
+ * {@link hu.bme.mit.theta.core.stmt.Stmts} to instantiate them.
  */
 
 package hu.bme.mit.theta.core.stmt;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/package-info.java
new file mode 100644
index 0000000000..515f94ecca
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/abstracttype/package-info.java
@@ -0,0 +1,24 @@
+/**
+ * Expressions that work with multiple types. Use {@link hu.bme.mit.theta.core.type.abstracttype.AbstractExprs}
+ * to create them. Note that these are abstract classes, and the corresponding expression for a given type will
+ * be created (e.g., integer addition).
+ *
+ * Arithmetic:
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.AddExpr}: addition
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.DivExpr}: division
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.MulExpr}: multiplication
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.SubExpr}: subtraction
+ *
+ * Comparison:
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.EqExpr}: equal
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.GeqExpr}: greater or equal
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.GtExpr}: greater
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.LeqExpr}: less or equal
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.LtExpr}: less
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.NeqExpr}: not equal
+ *
+ * Other
+ * - {@link hu.bme.mit.theta.core.type.abstracttype.CastExpr}: cast
+ */
+
+package hu.bme.mit.theta.core.type.abstracttype;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/anytype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/anytype/package-info.java
new file mode 100644
index 0000000000..877c32357b
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/anytype/package-info.java
@@ -0,0 +1,9 @@
+/**
+ * Expressions that work with any type. Use {@link hu.bme.mit.theta.core.type.anytype.Exprs} to create them.
+ *
+ * - {@link hu.bme.mit.theta.core.type.anytype.IteExpr}: conditional expression, e.g., if x > 0 then x else -x
+ * - {@link hu.bme.mit.theta.core.type.anytype.PrimeExpr}: primed expression, e.g., x'
+ * - {@link hu.bme.mit.theta.core.type.anytype.RefExpr}: reference to a declaration, e.g., x
+ */
+
+package hu.bme.mit.theta.core.type.anytype;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java
new file mode 100644
index 0000000000..c0a04644ee
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/package-info.java
@@ -0,0 +1,17 @@
+/**
+ * SMT array type and its expressions. Use {@link hu.bme.mit.theta.core.type.arraytype.ArrayExprs} to create them.
+ * SMT arrays are unbounded, associative mappings from a key type to a value type.
+ *
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayType}: the actual array type
+ *
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr}: array literal
+ *
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr}: read array at an index, e.g., a[i]
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr}: write array at an index, e.g., a[i <- v],
+ *   the result of write is a new array, where element i is v
+ *
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr}: equal
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr}: not equal
+ */
+
+package hu.bme.mit.theta.core.type.arraytype;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/package-info.java
new file mode 100644
index 0000000000..56ffc44230
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/booltype/package-info.java
@@ -0,0 +1,20 @@
+/**
+ * Bool type and its expressions. Use {@link hu.bme.mit.theta.core.type.booltype.BoolExprs} to create them.
+ *
+ * - {@link hu.bme.mit.theta.core.type.booltype.BoolType}: the actual Boolean type
+ *
+ * - {@link hu.bme.mit.theta.core.type.booltype.TrueExpr}: true literal
+ * - {@link hu.bme.mit.theta.core.type.booltype.FalseExpr}: false literal
+ *
+ * - {@link hu.bme.mit.theta.core.type.booltype.NotExpr}: negation
+ * - {@link hu.bme.mit.theta.core.type.booltype.AndExpr}: and (conjunction)
+ * - {@link hu.bme.mit.theta.core.type.booltype.OrExpr}: or (disjunction)
+ * - {@link hu.bme.mit.theta.core.type.booltype.ImplyExpr}: implication
+ * - {@link hu.bme.mit.theta.core.type.booltype.XorExpr}: exclusive or (xor)
+ * - {@link hu.bme.mit.theta.core.type.booltype.IffExpr}: equivalence (if and only if)
+ *
+ * - {@link hu.bme.mit.theta.core.type.booltype.ExistsExpr}: existential quantifier
+ * - {@link hu.bme.mit.theta.core.type.booltype.ForallExpr}: universal quantifier
+ */
+
+package hu.bme.mit.theta.core.type.booltype;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/package-info.java
new file mode 100644
index 0000000000..6d13a4bc81
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/package-info.java
@@ -0,0 +1,28 @@
+/**
+ * Integer type and its expressions. Use {@link hu.bme.mit.theta.core.type.inttype.IntExprs} to create them.
+ * Note that this is a (mathematical) SMT integer, with an unbounded range (long in the implementation) and
+ * no overflows.
+ *
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntType}: the actual integer type.
+ *
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntLitExpr}: integer literal
+ *
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntNegExpr}: unary minus
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntAddExpr}: addition
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntSubExpr}: subtraction
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntMulExpr}: multiplication
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntDivExpr}: integer division
+ * - {@link hu.bme.mit.theta.core.type.inttype.ModExpr}: modulus
+ * - {@link hu.bme.mit.theta.core.type.inttype.RemExpr}: remainder
+ *
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntEqExpr}: equal
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntNegExpr}: not equal
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntGtExpr}: greater
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntLtExpr}: less
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntGeqExpr}: greater or equal
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntLeqExpr}: less or equal
+ *
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntToRatExpr}: cast to rational
+ */
+
+package hu.bme.mit.theta.core.type.inttype;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/package-info.java
index d81047bd27..7472e6ed8b 100644
--- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/package-info.java
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/package-info.java
@@ -4,14 +4,16 @@
  * grouped into subpackages. Constructors of the types and expressions are
  * usually package private. Use the factory classes instead.
  *
- * @see hu.bme.mit.theta.core.type.anytype.Exprs
- * @see hu.bme.mit.theta.core.type.arraytype.ArrayExprs
- * @see hu.bme.mit.theta.core.type.booltype.BoolExprs
- * @see hu.bme.mit.theta.core.type.functype.FuncExprs
- * @see hu.bme.mit.theta.core.type.inttype.IntExprs
- * @see hu.bme.mit.theta.core.type.pointertype.PointerExprs
- * @see hu.bme.mit.theta.core.type.proctype.ProcExprs
- * @see hu.bme.mit.theta.core.type.rattype.RatExprs
+ * - {@link hu.bme.mit.theta.core.type.Expr} is the main interface for expressions.
+ * - {@link hu.bme.mit.theta.core.type.anytype.Exprs} and {@link hu.bme.mit.theta.core.type.abstracttype.AbstractExprs}
+ *   work for multiple types (e.g., conditional).
+ * - {@link hu.bme.mit.theta.core.type.booltype.BoolExprs} can create Boolean type and expressions (e.g., and, or).
+ * - {@link hu.bme.mit.theta.core.type.inttype.IntExprs} can create mathematical (SMT) integer type and expressions
+ *   (e.g., add, multiply).
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatExprs} can create rational type and expression (e.g., division).
+ * - {@link hu.bme.mit.theta.core.type.arraytype.ArrayExprs} can create SMT array type (associative mapping from a
+ *   key type to a value type) and expressions (e.g., read, write).
+ * - {@link hu.bme.mit.theta.core.type.functype.FuncExprs} can create function type and expressions.
  */
 
 package hu.bme.mit.theta.core.type;
\ No newline at end of file
diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/package-info.java
new file mode 100644
index 0000000000..79dd1f929a
--- /dev/null
+++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/package-info.java
@@ -0,0 +1,22 @@
+/**
+ * Rational type and its expressions. Use {@link hu.bme.mit.theta.core.type.rattype.RatExprs} to create them.
+ *
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatType}: the actual rational type
+ *
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatLitExpr}: rational literal, e.g., 1%2 is 0.5
+ *
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatNegExpr}: unary minus
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatAddExpr}: addition
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatSubExpr}: subtraction
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatMulExpr}: multiplication
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatDivExpr}: rational division
+ *
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatEqExpr}: equal
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatNeqExpr}: not equal
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatGtExpr}: greater
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatLtExpr}: less
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatGeqExpr}: greater or equal
+ * - {@link hu.bme.mit.theta.core.type.rattype.RatLeqExpr}: less or equal
+ */
+
+package hu.bme.mit.theta.core.type.rattype;
\ No newline at end of file