cvc5: A Versatile and Industrial-Strength SMT Solver

Haniel Barbosa,Clark Barrett,Martin Brain,Gereon Kremer,Hanna Lachnitt,Makai Mann, Abdalrhman Mohamed,Mudathir Mohamed,Aina Niemetz,Andres Notzli,Alex Ozdemir,Mathias Preiner,Andrew Reynolds,Ying Sheng,Cesare Tinelli,Yoni Zohar

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I（2022）

引用 86|浏览52

暂无评分

摘要

cvc5 is the latest SMT solver in the cooperating validity checker series and builds on the successful code base of CVC4. This paper serves as a comprehensive system description of cvc5's architectural design and highlights the major features and components introduced since CVC4 1.8. We evaluate cvc5's performance on all benchmarks in SMT-LIB and provide a comparison against CVC4 and Z3.

查看译文

关键词

automated reasoning, constraint solving, satisfiability modulo theories, cvc5

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要