Scholarlink

We present a new floating-point arithmetic (FPA) theory solver implemented in the cvc5 SMT solver. Differently from the major bit-blasting method, we use a real-blasting method that reasons about FPA formulas in a theory of real-integer arithmetic (RIA). It is based on an axiomatization of FPA operations with a set of conditional RIA formulas. The solver is implemented as an extended theory solver tightly coupled with cvc5 so that fragments of axioms are lazily instantiated regarding the solving context. Experimental results show that our solver performs better than existing solvers for several problem instances.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Real-Blasting Extension of cvc5 for Reasoning About Floating-Point Arithmetic

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Daisuke Ishii

摘要

We present a new floating-point arithmetic (FPA) theory solver implemented in the cvc5 SMT solver. Differently from the major bit-blasting method, we use a real-blasting method that reasons about FPA formulas in a theory of real-integer arithmetic (RIA). It is based on an axiomatization of FPA operations with a set of conditional RIA formulas. The solver is implemented as an extended theory solver tightly coupled with cvc5 so that fragments of axioms are lazily instantiated regarding the solving context. Experimental results show that our solver performs better than existing solvers for several problem instances.