[WIP] Use a separate Parikh Theory for handling length abstractions

.github/workflows/scala.yml

@@ -0,0 +1,22 @@
+name: Scala CI
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up JDK 11
+      uses: actions/setup-java@v2
+      with:
+        java-version: '11'
+        distribution: 'adopt'
+    - name: Run tests
+      run: sbt test

.gitignore

@@ -0,0 +1,7 @@
+/target
+.bloop
+/.bsp
+/.metals
+.DS_Store
+/project/project
+/project/target

.sbtconfig

@@ -0,0 +1,3 @@
+SBT_OPTS="-Xms4G -Xmx4G -Xss2M 
+ -XX:+CMSClassUnloadingEnabled 
+ -XX:MaxPermSize=4G"

.scalafmt.conf

@@ -0,0 +1,6 @@
+maxColumn = 80
+version=2.2.1
+project.git = true
+docstrings = "JavaDoc"
+# rewrite.rules = [SortImports]
+spaces.beforeContextBoundColon=Always

.vscode/launch.json

@@ -0,0 +1,23 @@
+{
+    // Use IntelliSense to learn about possible attributes.
+    // Hover to view descriptions of existing attributes.
+    // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "type": "scala",
+            "request": "launch",
+            "name": "Run tests",
+            "testClass": "ostrich.APITest",
+            "buildTarget": "root"
+        },
+        {
+            "type": "scala",
+            "name": "Debug ostrich.OstrichMain",
+            "request": "launch",
+            "mainClass": "ostrich.OstrichMain",
+            "buildTarget": "root",
+            "args": ["+quiet", "-stringSolver=ostrich.OstrichStringTheory:+eager", "tests/concat-regex.smt2"]
+        }
+    ]
+}

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "files.watcherExclude": {
+        "**/target": true
+    }
+}

README.md

@@ -1,4 +1,4 @@
-# OSTRICH [![Build Status](https://travis-ci.org/uuverifiers/ostrich.svg?branch=master)](https://travis-ci.org/uuverifiers/ostrich)
+# OSTRICH
 ## An SMT Solver for String Constraints
 
 OSTRICH is an SMT solver for string constraints.

build.sbt

@@ -2,23 +2,36 @@ lazy val commonSettings = Seq(
   name := "ostrich",
   organization := "uuverifiers",
   version := "1.0",
-  scalaVersion := "2.11.12",
-  crossScalaVersions := Seq("2.11.12", "2.12.10"),
-  publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) ),
-  scalacOptions += "-deprecation",
-  resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/").withAllowInsecureProtocol(true),
-  libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
-  libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.4-SNAPSHOT",
-  libraryDependencies += "org.sat4j" % "org.sat4j.core" % "2.3.1",
+  scalaVersion := "2.13.5",
+  publishTo := Some(
+    Resolver.file("file", new File("/home/wv/public_html/maven/"))
+  ),
+  scalacOptions ++= Seq(
+    "-deprecation",
+    //"-Xfatal-warnings",
+    "-unchecked",
+    "-Xlint",
+    "-Xelide-below",
+    "INFO",
+    "-feature",
+    "-opt-inline-from:**",
+    "-opt:l:method",
+    "-opt:l:inline",
+    "-Ywarn-dead-code",
+    "-Ywarn-unused"
+  ),
+  resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/")
+    .withAllowInsecureProtocol(true),
+  libraryDependencies += "uuverifiers" %% "princess" % "nightlySNAPSHOT",
+  libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
-  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8"
+  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8",
+  libraryDependencies += "uuverifiers" %% "parikh-theory" % "0.1.0-SNAPSHOT"
 )
 
-lazy val root = (project in file(".")).
-  settings(commonSettings: _*).
-  settings(
-    mainClass in Compile := Some("ostrich.OstrichMain"),
-    unmanagedSourceDirectories in Test += baseDirectory.value / "replaceall-benchmarks" / "src" / "test" / "scala"
-  )
-
-
+lazy val root = (project in file("."))
+  .settings(commonSettings: _*)
+  .settings(
+    Compile / mainClass := Some("ostrich.OstrichMain"),
+    Test / unmanagedSourceDirectories += baseDirectory.value / "replaceall-benchmarks" / "src" / "test" / "scala"
+  )

ostrich

@@ -20,7 +20,7 @@ ostrichParams=""
 
 for p; do
     case "$p" in
-        [+-]eager | [+-]forward | -length=*)
+        [+-]eager | [+-]forward | -length=* | [+-]minimizeAutomata)
             if [ x"$ostrichParams" = x"" ]; then
                 ostrichParams=$p
             else

ostrich-client

@@ -88,7 +88,7 @@ until [ $success -eq 0 ]; do
 
         for var; do
 	    case "$var" in
-                [+-]eager | [+-]forward | -length=*)
+                [+-]eager | [+-]forward | -length=* | [+-]minimizeAutomata)
                     if [ x"$ostrichParams" = x"" ]; then
                         ostrichParams=$var
                     else

project/build.properties

@@ -1 +1 @@
-sbt.version=1.4.0
+sbt.version=1.5.3

project/metals.sbt

@@ -0,0 +1,4 @@
+// DO NOT EDIT! This file is auto-generated.
+// This file enables sbt-bloop to create bloop config files.
+
+addSbtPlugin("ch.epfl.scala" % "sbt-bloop" % "1.4.8-19-4d9f966b")

src/main/scala/ostrich/AutDatabase.scala

@@ -57,12 +57,15 @@ object AutDatabase {
  * regular expressions. The database will assign a unique id to regular
  * expressions, and will compute the resulting automaton on demand.
  */
-class AutDatabase(theory : OstrichStringTheory) {
+class AutDatabase(theory : OstrichStringTheory,
+                  minimizeAutomata : Boolean) {
 
   import AutDatabase._
 
   private val regex2Aut  = new Regex2Aut(theory)
 
+  private var nextId     = 0
+
   private val regexes    = new MHashMap[ITerm, Int]
   private val id2Regex   = new MHashMap[Int, ITerm]
   private val id2Aut     = new MHashMap[Int, Automaton]
@@ -77,11 +80,23 @@ class AutDatabase(theory : OstrichStringTheory) {
   def regex2Id(regexTerm : ITerm) : Int =
     synchronized {
       regexes.getOrElseUpdate(regexTerm, {
-                                val id = regexes.size
+                                val id = nextId
+                                nextId = nextId + 1
                                 id2Regex.put(id, regexTerm)
                                 id })
     }
 
+  /**
+   * Add a new automaton to the database.
+   */
+  def automaton2Id(aut : Automaton) : Int =
+    synchronized {
+      val id = nextId
+      nextId = nextId + 1
+      id2Aut.put(id, aut)
+      id
+    }
+
   /**
    * Query the id of a regular expression.
    */
@@ -100,7 +115,7 @@ class AutDatabase(theory : OstrichStringTheory) {
         case None =>
           (id2Regex get id) match {
             case Some(regex) => {
-              val aut = regex2Aut buildAut regex
+              val aut = regex2Aut.buildAut(regex, minimizeAutomata)
               id2Aut.put(id, aut)
               Some(aut)
             }
@@ -110,6 +125,13 @@ class AutDatabase(theory : OstrichStringTheory) {
       }
     }
 
+  /**
+   * Query the automaton that belongs to the regular expression with given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2AutomatonBE(id : Int) : Option[Automaton] =
+    synchronized { id2Aut get id }
+
   /**
    * Query the complemented automaton that belongs to the regular
    * expression with given id.
@@ -131,6 +153,14 @@ class AutDatabase(theory : OstrichStringTheory) {
       }
     }
 
+  /**
+   * Query the complemented automaton that belongs to the regular
+   * expression with given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2ComplementedAutomatonBE(id : Int) : Option[Automaton] =
+    synchronized { id2CompAut get id }
+
   /**
    * Query the automaton that belongs to the regular expression with
    * given id.
@@ -140,6 +170,16 @@ class AutDatabase(theory : OstrichStringTheory) {
     case ComplementedAut(id) => id2ComplementedAutomaton(id)
   }
 
+  /**
+   * Query the automaton that belongs to the regular expression with
+   * given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2AutomatonBE(id : NamedAutomaton) : Option[Automaton] = id match {
+    case PositiveAut(id)     => id2AutomatonBE(id)
+    case ComplementedAut(id) => id2ComplementedAutomatonBE(id)
+  }
+
   /**
    * Check whether <code>aut1</code> specifies a subset of <code>aut2</code>.
    */
@@ -160,6 +200,30 @@ class AutDatabase(theory : OstrichStringTheory) {
       true
     }
 
+  /**
+   * Check whether <code>aut1</code> specifies a subset of <code>aut2</code>;
+   * the check is only carried out when all required automata are already in
+   * the database.
+   */
+  def isSubsetOfBE(aut1 : NamedAutomaton,
+                   aut2 : NamedAutomaton) : Option[Boolean] =
+    if (aut1.id < aut2.id) {
+      synchronized {
+        // aut1 <= aut2
+        //  <==>
+        // (aut1 & aut2.complement) = empty
+        for (a1 <- id2AutomatonBE(aut1);
+             a2 <- id2AutomatonBE(aut2.complement)) yield 
+          subsetRel.getOrElseUpdate((aut1, aut2),
+                                    !AutomataUtils.areConsistentAutomata(
+                                      List(a1, a2)))
+      }
+    } else if (aut1.id > aut2.id) {
+      isSubsetOfBE(aut2.complement, aut1.complement)
+    } else {
+      Some(true)
+    }
+
   /**
    * Check whether <code>aut1</code> and <code>aut2</code> have empty
    * intersection.

src/main/scala/ostrich/AutomataAdapters.scala

@@ -67,7 +67,7 @@ abstract class AtomicStateAutomatonAdapter[A <: AtomicStateAutomaton]
   def unary_! : Automaton =
     !intern(this)
 
-  def isEmpty : Boolean =
+  override def isEmpty : Boolean =
     !AutomataUtils.areConsistentAtomicAutomata(List(this))
 
   def apply(word : Seq[Int]) : Boolean =