Z3str3: A String Solver With Theory-Aware Heuristics
PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017)(2017)
摘要
We present a new string SMT solver, Z3str3, that is faster than its competitors Z3str2, Norn, CVC4, S3, and S3P over a majority of three industrial-strength benchmarks, namely, Kaluza, PISA, and IBM AppScan. Z3str3 supports string equations, linear arithmetic over length function, and regular language membership predicate. The key algorithmic innovation behind the efficiency of Z3str3 is a technique we call theory-aware branching, wherein we modify Z3's branching heuristic to take into account the structure of theory literals to compute branching activities. In the traditional DPLL(T) architecture, the structure of theory literals is hidden from the DPLL(T) SAT solver because of the Boolean abstraction constructed over the input theory formula. By contrast, the theory-aware technique presented in this paper exposes the structure of theory literals to the DPLL(T) SAT solver's branching heuristic, thus enabling it to make much smarter decisions during its search than otherwise. As a consequence, Z3str3 has better performance than its competitors.
更多查看译文
关键词
branching activities,input theory formula,theory-aware technique,theory-aware heuristics,string SMT solver,Z3str2,CVC4,S3P,industrial-strength benchmarks,IBM AppScan,string equations,linear arithmetic,length function,regular language membership predicate,key algorithmic innovation,theory-aware branching,ZSstrS,Norn,Z3 branching heuristic,theory literal structure,DPLL(T) architecture,Boolean abstraction,DPLL(T) SAT solver branching heuristic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络