[Ostrich] String theory crashes when solving query with STR_LESS_EQUAL

[kfriedberger]

❗ Maybe the following is a bug for Ostrich. Then please move this issue to a better place.

The JavaSMT developers are currently trying to improve their support for String/Regex theory with the SMT solver Princess (see sosy-lab/java-smt#257). There are some smaller issues in Princess (version 2023-06-19) that block us from a good integration.

The following issue appeared when solving a smaller formula for String theory:

Description:

We want to solve the query "a" <= var && var <= "c" && len(var) == 1 and want to proove that var is one of ["a", "b", "c"]. (The original query uses STR_LESS_THAN rather than STR_LESS_EQUAL, which limits the result to var:="b".)

Code / Junit test:

Please note that the interaction between Java and Scala is not nice to read 😄 .

  private StringTheory stringTheory;
  private SimpleAPI api;

  @Before
  public void init() {
    api = SimpleAPI.apply(
            SimpleAPI.apply$default$1(),
            SimpleAPI.apply$default$2(),
            SimpleAPI.apply$default$3(),
            SimpleAPI.apply$default$4(),
            SimpleAPI.apply$default$5(),
            SimpleAPI.apply$default$6(),
            SimpleAPI.apply$default$7(),
            SimpleAPI.apply$default$8(),
            SimpleAPI.apply$default$9(),
            SimpleAPI.apply$default$10(),
            SimpleAPI.apply$default$11());
    stringTheory = new OstrichStringTheory(
        collectionAsScalaIterableConverter(new ArrayList<Tuple2<String, Transducer>>()).asScala().toSeq(),
        new OFlags(
            OFlags.$lessinit$greater$default$1(),
            OFlags.$lessinit$greater$default$2(),
            OFlags.$lessinit$greater$default$3(),
            OFlags.$lessinit$greater$default$4(),
            OFlags.$lessinit$greater$default$5(),
            OFlags.$lessinit$greater$default$6(),
            OFlags.$lessinit$greater$default$7(),
            OFlags.$lessinit$greater$default$8(),
            OFlags.$lessinit$greater$default$9(),
            OFlags.$lessinit$greater$default$10(),
            OFlags.$lessinit$greater$default$11(),
            OFlags.$lessinit$greater$default$12()));
  }

  @Test
  public void testStringTheory() {
    ITerm a = stringTheory.string2Term("a");
    ITerm c = stringTheory.string2Term("c");
    ITerm var = api.createConstant("var", stringTheory.StringSort());
    ITerm num1 = new IIntLit(IdealInt.apply(1));

    IFormula a_le_var = new IAtom(stringTheory.str_$less$eq(), collectionAsScalaIterableConverter(List.of(a, var)).asScala().toSeq());
    IFormula var_le_c = new IAtom(stringTheory.str_$less$eq(), collectionAsScalaIterableConverter(List.of(var, c)).asScala().toSeq());
    IFormula var_of_len_one = num1.$eq$eq$eq(new IFunApp(stringTheory.str_len(), collectionAsScalaIterableConverter(List.of(var)).asScala().toSeq()));

    api.addAssertion(a_le_var);
    api.addAssertion(var_le_c);
    api.addAssertion(var_of_len_one);
    Value result = api.checkSat(true); // --> CRASH instead of SAT
  }
}

Stacktrace:

ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: java.lang.Exception: Cannot handle literal char_<=(var, 2)
	at ap.api.SimpleAPI.ap$api$SimpleAPI$$evalProverResult(SimpleAPI.scala:2146)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1(SimpleAPI.scala:2082)
	at ap.api.SimpleAPI.$anonfun$getOrUpdateLastStatus$1$adapted(SimpleAPI.scala:2082)
	at scala.Option.foreach(Option.scala:437)
	at ap.api.SimpleAPI.getOrUpdateLastStatus(SimpleAPI.scala:2082)
	at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2088)
	at ap.api.SimpleAPI.getStatusWithDeadline(SimpleAPI.scala:2062)
	at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:1985)
	at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1913)
	at ... <insert code position from above>
Caused by: java.lang.Exception: Cannot handle literal char_<=(var, 2)
	at ostrich.OstrichSolver.$anonfun$findStringModel$1(OstrichSolver.scala:189)
	at scala.collection.immutable.Vector.foreach(Vector.scala:1856)
	at ostrich.OstrichSolver.findStringModel(OstrichSolver.scala:162)
	at ostrich.OstrichStringTheory$$anon$1.$anonfun$callBackwardProp$1(OstrichStringTheory.scala:382)
	at ap.util.LRUCache.apply(LRUCache.scala:49)
	at ostrich.OstrichStringTheory$$anon$1.callBackwardProp(OstrichStringTheory.scala:382)
	at ostrich.OstrichStringTheory$$anon$1.$anonfun$handleGoal$6(OstrichStringTheory.scala:369)
	at ap.proof.theoryPlugins.TheoryProcedure$RichActionSeq.elseDo(Plugin.scala:197)
	at ostrich.OstrichStringTheory$$anon$1.handleGoal(OstrichStringTheory.scala:369)
	at ap.proof.theoryPlugins.PluginSequence.handleGoal(Plugin.scala:275)
	at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:435)
	at ap.proof.goal.Goal.step(Goal.scala:421)
	at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:487)
	at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1113)
	at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:157)
	at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
	at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:158)
	at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
	at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:213)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
	at ap.util.Timeout$.withChecker(Timeout.scala:56)
	at ap.api.ProofThreadRunnable.run(ProofThread.scala:203)
	at java.base/java.lang.Thread.run(Thread.java:833)

[pruemmer]

Thanks for the bug report. This was a missing case in Ostrich, which has now been fixed on the Ostrich master.

[kfriedberger]

@pruemmer Would it be possible to provide a recent release of Ostrich? Thanks in advance.

[pruemmer]

Sorry for the delay; I have now published a version 1.3.5 that includes those fixes!