使用Z3和SMT-LIB定义实数的sqrt函数 [英] Use Z3 and SMT-LIB to define sqrt function with a real number

问题描述

我如何以 smt-libv2 格式编写 sqrt 函数.

How I can write sqrt function in smt-libv2 format.

注意:为了获得最多两个值，我在这里找到了一个有用的链接:使用 Z3 和 SMT-LIB 获得最多两个值.

Note: To get a maximum of two values, i found a useful link here: Use Z3 and SMT-LIB to get a maximum of two values.

推荐答案

假设您的公式没有量词，那么您可以通过引入新变量和添加约束来隐式定义平方根.例如你可以写:

Suppose that your formula is quantifier free, then you can define square-roots implicitly by introducing fresh variables and adding constraints. For example you can write:

  (define-fun is_sqrt ((x Real) (y Real)) Bool (= y (* x x)))

那么'x'就是'y'的平方根；如果你只想要非负平方根，那么:

Then 'x' is a square root of 'y'; and if you just want the non-negative square roots, then:

  (define-fun is_sqrt ((x Real) (y Real)) Bool (and (>= x 0) (= y (* x x))))

对于断言中出现平方根的每个事件，引入一个新变量并将新变量插入该位置.然后添加断言

For every occurrence in your assertion where you have a square root, introduce a fresh variable and plug the fresh variable into that place. Then add the assertion

   (assert (is_sqrt fresh-variable sub-term))

Z3 还提供了一个内置运算符，用于将项提升为幂.您可以使用它来获得平方根.所以要写出'x'的平方根，你可以写这个词:

Z3 also provides a built-in operator for lifting terms into a power. You can use this to get a square root. So to write the square root of 'x', you can write the term:

   (^ x 0.5)

在 Z3 中使用幂的推理在某种程度上受到限制，因此这实际上取决于您的公式所说的内容是否会以与关系编码相同的方式处理此公式.

The inference using powers in Z3 is somewhat limited, so it really depends on what your formula says whether this formulation will be handled in the same way as the relational encoding.

这篇关于使用Z3和SMT-LIB定义实数的sqrt函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！