SAT-check for String theory with codepoint crashes in MatchError

[kfriedberger]

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

The following issue appeared in a simple SAT check:

Description:
We want to assert a formula string::codepoint(x) == string::codepoint(x) with a simple integer symbol x. Princess crashes. 😢

Java code (partial):

    SimpleAPI api = SimpleAPI.apply(...default args...);
    StringTheory stringTheory = new OstrichStringTheory(toSeq(new ArrayList<>()), new OFlags(...default args...));

    ITerm var = api.createConstant("x", Integer$.MODULE$);
    IFunApp cp = new IFunApp(stringTheory.str_from_code(), toITermSeq(var));
    IFormula eq = cp.$eq$eq$eq(cp);
    api.addAssertion(eq);
    Value result = api.checkSat(true); // --> CRASH

Stacktrace:

scala.MatchError: str_cons(cp, 0) (of class ap.parser.IFunApp)
	at ostrich.StrDatabase.iTerm2Id(StrDatabase.scala:172)
	at ostrich.OstrichStringEncoder.postVisit(OstrichPreprocessor.scala:457)
	at ostrich.OstrichStringEncoder.postVisit(OstrichPreprocessor.scala:440)
	at ap.parser.CollectingVisitor.visit(InputAbsyVisitor.scala:126)
	at ostrich.OstrichStringEncoder.apply(OstrichPreprocessor.scala:446)
	at ostrich.OstrichStringTheory.iPreprocess(OstrichStringTheory.scala:488)
	at ap.theories.Theory$.$anonfun$iPreprocess$1(Theory.scala:135)
	at scala.collection.immutable.List.foldRight(List.scala:353)
	at scala.collection.IterableOnceOps.$colon$bslash(IterableOnce.scala:761)
	at scala.collection.IterableOnceOps.$colon$bslash$(IterableOnce.scala:761)
	at scala.collection.AbstractIterable.$colon$bslash(Iterable.scala:935)
	at ap.theories.Theory$.iPreprocess(Theory.scala:135)
	at ap.parser.Preprocessing$.$anonfun$apply$3(Preprocessing.scala:99)
	at scala.collection.immutable.List.map(List.scala:247)
	at ap.parser.Preprocessing$.apply(Preprocessing.scala:98)
	at ap.api.SimpleAPI.toInternal(SimpleAPI.scala:4272)
	at ap.api.SimpleAPI.flushTodo(SimpleAPI.scala:4034)
	at ap.api.SimpleAPI.checkSatHelp(SimpleAPI.scala:1960)
	at ap.api.SimpleAPI.checkSat(SimpleAPI.scala:1946)

[pruemmer]

At the moment, Ostrich does not support the use of the `str.from_code` function with a symbolic argument. The only way to create an equation of this kind is to use a string variable x and assert that its length is 1. We could relatively easily rewrite such terms in the preprocessing, however, if this functionality is important for you.

[kfriedberger]

JavaSMT does not want to introduce additional utility symbols and equations. Integrating this functionality directly within Princess/Ostrich would be beneficial. This enhancement is not a high priority for us, so its implementation can be deferred.