Extend core docs, fix stmt parsing

subprojects/core/README.md

@@ -1,4 +1,4 @@
-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.
+This project provides classes and utilities to build and manipulate first order logic (FOL) expressions, statements and related concepts, which serve as a basis for the formalisms and analyses.
 
 Classes include
 * types (e.g., Boolean, integer, rational, array),
@@ -12,4 +12,5 @@ see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/model/package-
 * 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.
+Utilities include folding, unfolding, collecting atoms, collecting variables, etc.,
+see the [`package-info.java`](src/main/java/hu/bme/mit/theta/core/utils/package-info.java) for more details.

subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/CoreDslManager.java

@@ -34,6 +34,9 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
 
+/**
+ * Utility class for parsing types, expressions and statements.
+ */
 public final class CoreDslManager {
 
 	private final BasicScope scope;
@@ -64,7 +67,7 @@ public Expr<?> parseExpr(final String string) {
 	public Stmt parseStmt(final String string) {
 		checkNotNull(string);
 		final CoreDslParser parser = createParserForString(string);
-		final ParseTree tree = parser.expr();
+		final ParseTree tree = parser.stmt();
 		return tree.accept(new StmtCreatorVisitor(scope));
 	}
 

subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/StmtCreatorVisitor.java

@@ -17,14 +17,14 @@
 
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
-import static hu.bme.mit.theta.core.stmt.Stmts.Assign;
-import static hu.bme.mit.theta.core.stmt.Stmts.Assume;
+import static hu.bme.mit.theta.core.stmt.Stmts.*;
 
 import hu.bme.mit.theta.common.dsl.Scope;
 import hu.bme.mit.theta.core.decl.Decl;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.dsl.DeclSymbol;
 import hu.bme.mit.theta.core.dsl.gen.CoreDslBaseVisitor;
+import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.HavocStmtContext;
 import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AssignStmtContext;
 import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AssumeStmtContext;
 import hu.bme.mit.theta.core.stmt.AssumeStmt;
@@ -64,4 +64,10 @@ public AssumeStmt visitAssumeStmt(final AssumeStmtContext ctx) {
 		return Assume(cond);
 	}
 
+	@Override
+	public Stmt visitHavocStmt(final HavocStmtContext ctx) {
+		@SuppressWarnings("unchecked") final VarDecl<Type> lhs = (VarDecl<Type>) resolveVar(scope, ctx.lhs.getText());
+		return Havoc(lhs);
+	}
+
 }

subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/package-info.java

@@ -1,8 +1,6 @@
 /**
  * This package contains the domain specific language (DSL) and the parser for
- * expressions.
- *
- * @see hu.bme.mit.theta.core.dsl.CoreDslManager
+ * expressions. Use {@link hu.bme.mit.theta.core.dsl.CoreDslManager} as the entry point.
  */
 
 package hu.bme.mit.theta.core.dsl;

subprojects/core/src/main/java/hu/bme/mit/theta/core/type/package-info.java

@@ -1,19 +1,20 @@
 /**
- * This package contains types (e.g., boolean, integer) and expressions
- * operating over them (e.g., boolean connectives, arithmetic operations),
+ * This package contains types (e.g., Boolean, integer) and expressions
+ * operating over them (e.g., Boolean connectives, arithmetic operations),
  * grouped into subpackages. Constructors of the types and expressions are
  * usually package private. Use the factory classes instead.
  *
  * - {@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
+ *
+ * - {@link hu.bme.mit.theta.core.type.anytype} and {@link hu.bme.mit.theta.core.type.abstracttype}
+ *   are expressions for multiple types (e.g., conditional).
+ * - {@link hu.bme.mit.theta.core.type.booltype} contains the Boolean type and expressions (e.g., and, or).
+ * - {@link hu.bme.mit.theta.core.type.inttype} contains the 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
+ * - {@link hu.bme.mit.theta.core.type.rattype} contains the rational type and expression (e.g., division).
+ * - {@link hu.bme.mit.theta.core.type.arraytype} contains the 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.
+ * - {@link hu.bme.mit.theta.core.type.functype} contains the function type and expressions.
  */
 
 package hu.bme.mit.theta.core.type;

subprojects/core/src/test/java/hu/bme/mit/theta/core/dsl/StmtDslTest.java

@@ -0,0 +1,58 @@
+package hu.bme.mit.theta.core.dsl;
+
+import hu.bme.mit.theta.core.decl.Decl;
+import hu.bme.mit.theta.core.decl.Decls;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.core.type.inttype.IntExprs;
+import hu.bme.mit.theta.core.type.inttype.IntType;
+import org.junit.Assert;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.Collections;
+
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.*;
+import static hu.bme.mit.theta.core.stmt.Stmts.*;
+
+@RunWith(Parameterized.class)
+public class StmtDslTest {
+    @Parameterized.Parameter(value = 0)
+    public String actual;
+
+    @Parameterized.Parameter(value = 1)
+    public Stmt expected;
+
+    @Parameterized.Parameter(value = 2)
+    public Collection<Decl<?>> decls;
+
+    private static VarDecl<IntType> x = Decls.Var("x", IntExprs.Int());
+
+    @Parameterized.Parameters
+    public static Collection<Object[]> data() {
+        return Arrays.asList(new Object[][]{
+
+                {"assume true", Assume(True()), null},
+
+                {"x := x + 1", Assign(x, Add(x.getRef(), Int(1))) , Collections.singleton(x)},
+
+                {"havoc x", Havoc(x) , Collections.singleton(x)}
+
+        });
+    }
+
+    @Test
+    public void test() {
+        final CoreDslManager manager = new CoreDslManager();
+
+        if (decls != null) {
+            decls.forEach(decl -> manager.declare(decl));
+        }
+
+        Assert.assertEquals(expected, manager.parseStmt(actual));
+    }
+}