Rebase interactive onto the current master

.gitignore

@@ -11,8 +11,7 @@ target/
 lib_managed/
 src_managed/
 project/boot/
-project/
-project/plugins/project/
+target/
 .history
 .cache
 .lib/
@@ -94,9 +93,6 @@ fabric.properties
 # Compiled class file
 *.class
 
-# Log file
-*.log
-
 # BlueJ files
 *.ctxt
 
@@ -118,9 +114,6 @@ hs_err_pid*
 *~
 .*.swp
 
-# stats
-*.csv
-
 # Emacs-generated
 .#*
 
@@ -151,4 +144,11 @@ node_modules
 # certification results
 certify/
 
+# logs, stats, and other outputs
+/logs
+*.log
+*.csv
 *results.tex
+trace.json
+*.trace.json
+*.db.json

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "ext/tutorial"]
+	path = ext/tutorial
+	url = https://github.com/TyGuS/suslik-tutorial.git

Aptfile

@@ -0,0 +1 @@
+z3

Procfile

@@ -0,0 +1 @@
+web: target/universal/stage/bin/synthesis-server

build.sbt

@@ -10,31 +10,38 @@ scalaVersion := "2.12.12"
 javacOptions ++= Seq("-source", "1.8", "-target", "1.8", "-Xlint")
 scalacOptions += "-target:jvm-1.8"
 
-resolvers in ThisBuild ++= Seq(
+ThisBuild / resolvers ++= Seq(
     Resolver.sonatypeRepo("releases"),
     Resolver.sonatypeRepo("snapshots")
 )
 
 resolvers += Resolver.bintrayIvyRepo("com.eed3si9n", "sbt-plugins")
 
+lazy val akkaHttpVersion = "10.2.4"
+lazy val akkaVersion    = "2.6.14"
+
 libraryDependencies ++= Seq(
   "org.slf4j" % "slf4j-api" % "1.6.4" withSources(),
   "ch.qos.logback" % "logback-classic" % "1.1.3" % "test",
   "org.scalatest" %% "scalatest" % "3.0.1" % "test",
-  "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.6" withSources(),
+  "org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2" withSources(),
   "org.scalaz" %% "scalaz-core" % "7.2.11",
   "com.github.scopt" %% "scopt" % "3.7.0",
   "com.typesafe.scala-logging" %% "scala-logging" % "3.7.2",
-  "com.lihaoyi" %% "upickle" % "0.9.5",
-  "org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.1.1-SNAPSHOT" withSources()
+  "com.lihaoyi" %% "upickle" % "1.3.15",
+  "org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.1.1-SNAPSHOT" withSources(),
+  // Server stuff
+  "com.typesafe.akka" %% "akka-http" % akkaHttpVersion,
+  "com.typesafe.akka" %% "akka-stream" % akkaVersion,
+  "com.typesafe.akka" %% "akka-actor-typed" % akkaVersion
 )
 
 scalacOptions ++= Seq()
 
-logLevel in ThisBuild := Level.Warn
+ThisBuild / logLevel := Level.Warn
 
 //  creating a logger and setting level to warn/whatever for console
-initialCommands in console :=
+console / initialCommands :=
     """|
        | import ch.qos.logback.classic.Logger
        | import org.slf4j.LoggerFactory
@@ -43,15 +50,16 @@ initialCommands in console :=
        | root.setLevel(Level.OFF)
        | """.stripMargin
 
-mainClass in assembly := Some("org.tygus.suslik.synthesis.SynthesisRunner")
-
-test in assembly := {}
+Test / parallelExecution := false
 
-parallelExecution in Test := false
+assembly / assemblyJarName := "suslik.jar"
+assembly / mainClass := Some("org.tygus.suslik.synthesis.SynthesisRunner")
+assembly / test := {}
 
-assemblyJarName in assembly := "suslik.jar"
-
-assemblyMergeStrategy in assembly := {
- case PathList("META-INF", xs @ _*) => MergeStrategy.discard
- case x => MergeStrategy.first
+assembly / assemblyMergeStrategy := {
+  case PathList("META-INF", _*) => MergeStrategy.discard
+  case x if Assembly.isConfigFile(x) => MergeStrategy.concat
+  case _ => MergeStrategy.first
 }
+
+enablePlugins(JavaAppPackaging)

logback.prod.xml

@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<configuration>
+  <logger name="org.bitbucket.franck44" level="ERROR"/>
+
+    <!-- Stop output INFO at start -->
+    <statusListener class="ch.qos.logback.core.status.NopStatusListener" />
+
+    <appender name="LOGFILE" class="ch.qos.logback.core.rolling.RollingFileAppender">
+        <file>logs/suslik-server.log</file>
+        <rollingPolicy class="ch.qos.logback.core.rolling.FixedWindowRollingPolicy">
+          <fileNamePattern>logs/suslik-server.%i.log.zip</fileNamePattern>
+          <minIndex>1</minIndex>
+          <maxIndex>30</maxIndex>
+        </rollingPolicy>
+
+        <triggeringPolicy class="ch.qos.logback.core.rolling.SizeBasedTriggeringPolicy">
+          <maxFileSize>50MB</maxFileSize>
+        </triggeringPolicy>
+        <encoder>
+          <pattern>%d{yyyy-MM-dd HH:mm:ss} [%thread] %-5level %logger{35} - %msg%n</pattern>
+        </encoder>
+    </appender>
+
+    <root level="info">
+        <appender-ref ref="LOGFILE"/>
+    </root>
+
+</configuration>