English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Case split is a core proof rule in current decision procedures for the theoryof string constraints. Its use is the primary cause of the state spaceexplosion in string constraint solving, since it is the only rule that createsbranches in the proof tree. Moreover, explicit handling of the case split rulemay cause recomputation of the same tasks in multiple branches of the prooftree. In this paper, we propose a symbolic algorithm that significantly reducessuch a redundancy. In particular, we encode a string constraint as a regularlanguage and proof rules as rational transducers. This allows us to performsimilar steps in the proof tree only once, alleviating the state spaceexplosion. We also extend the encoding to handle arbitrary Boolean combinationsof string constraints, length constraints, and regular constraints. In ourexperimental results, we validate that our technique works in many practicalcases where other state-of-the-art solvers fail to provide an answer; ourPython prototype implementation solved over 50 % of string constraints thatcould not be solved by the other tools.

A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)