uuverifiers
SAT-check for String theory with codepoint crashes in MatchError
The JavaSMT developers are currently trying to improve their support for String theory with the SMT solver Princess (see https://github.com/sosy-lab/java-smt/pull/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)
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.
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.
The function str_from_code should work as expected by now, both in the string back-end of Princess and in Ostrich.