PV4 ⊧ Z3str3REpart of Z3, produces a satisfiability result for a set of constrains

Algorithm for SMT solving

Implemented as part of Z3 for solving regex constraints and linear integer arithmetic over length of string terms.

Artifact/reproduction package for CAV '21 paper: https://figshare.com/s/5ae73a6f3c55f5c5e4c1

15 July 2021

Other string solvers: CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau
SMT solvers that support theories over regular expression membership predicate and linear arithmetic over length of strings: CVC4, Z3str3, Norn, S3P, HAMPI