Proving formulas with no singleton Strings

[daniel-raffler]

Hello Ostrich seems to struggle with Formulas that don't contain a singleton String. Here is an example:

import ap.theories.strings.StringTheory
import ap.SimpleAPI
import SimpleAPI.ProverStatus
import ap.parser._
import ap.theories.strings.SeqStringTheory
import ap.util.Debug
import ostrich.{OstrichStringTheory, OFlags}

import org.scalacheck.{Arbitrary, Gen, Properties}
import org.scalacheck.Prop._

object Bug2 extends Properties("Bug2") {
  Debug enableAllAssertions true

  val stringTheory = new OstrichStringTheory(List(), OFlags())
  import stringTheory._
  import IExpression._

  property("lessThan") =
    SimpleAPI.withProver(enableAssert = true) { p =>
      import p._
      val a, b = createConstant(StringSort)
      !!(str_<=(a,b))
      ??? == ProverStatus.Sat
    }
}

When I run the progam Ostrich will throw an exception:

Exception: ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.Exception:
Cannot handle literal str_<=(c0, c1)

Is this the intended behavior, or am I doing something wrong here?

The program does work just fine when one of the arguments tostr.<= is replaced with a singleton String. Would it be possible to add support for arguments that are not singleton Strings? Or is this just one of the limitations of the algorithm that is being used?

[pruemmer]

This is a restriction of the current solver architecture. We are in the process of revising and reimplementing the theory solver, and the new version will be able to solve this constraint.

[daniel-raffler]

Hello Philipp, great to hear that this is already being worked on! I've wrapped up most of the issues we've had with Princess/Ostrich and hope that we can merge https://github.com/sosy-lab/java-smt/pull/257 soon. Once your new version is ready it should be enough to simply update the dependency.