We introduce TRAU, an SMT solver for an expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem for such a class of constraints is in general undecidable. The key idea behind TRAU is a technique called flattening, which searches for satisfying assignments that follow simple patterns. TRAU implements a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under- and an over-approximation module. The approximations are refined in an automatic manner by information flow between the two modules. The technique implemented by TRAU can handle a rich class of string constraints and has better performance than state-of-the-art string solvers.
Funding Agencies|Swedish Research Council (VR)Swedish Research Council [2014-5484]; Swedish Foundation for Strategic Research (SSF)Swedish Foundation for Strategic Research [RIT17-0011]; Czech Science FoundationGrant Agency of the Czech Republic [16-24707Y]; IT4IXS: IT4Innovations Excellence in Science project [LQ1602]; FIT BUT [FIT-S-17-4014]; Ministry of Science and Technology of TaiwanMinistry of Science and Technology, Taiwan [106-2221-E-001-009-MY3]