z3python:使用数学库 [英] z3python: using math library

问题描述

我试图在z3python中使用python的数学库，

I was trying to use python's math library with z3python, what I did was

import z3
import math
a,b = z3.Reals('a b')
solve(b == math.factorial(a), b == 6)

它返回的错误消息是AttributeError:ArithRef实例没有属性" float ".

The error message it returns is AttributeError: ArithRef instance has no attribute 'float'.

我的目的不是真的在Z3中使用阶乘函数，而是我很好奇数学库中的函数是否可以与Z3一起使用.任何建议表示赞赏.

My purpose is not really using the factorial function in Z3, rather I am curious if the functions from the math library can be used with Z3 in general. Any suggestion is appreciated.

推荐答案

通常，不能，这是不可能的.原因是Python函数无法转换为逻辑约束(理论上可以通过此处. a>).

In general, no, this is not possible. The reason is that there is no translation for Python functions to logical constraints (which in theory could be done, e.g., via the fixed-point engine), but it would require substantial effort and essentially an encoding of (in general undecidable) model-checking problems. See also Leo's excellent answer to a related question here).

在此特定示例中，请注意a是符号，即它表示任何可能的实数. math.factorial不知道如何处理此信息，因为它的实现仅处理具体的实数.

In this particular example, note that a is symbolic, i.e., it represents any possible real number. math.factorial does not know what to do with this information, because it's implementation only handles concrete real numbers.

对于某些特定功能，当然可以为Z3提供精确的编码.例如，Z3支持幂运算，而Python API提供了__pow__运算符.但是请注意，此运算符的语义可能与Python的__pow__在实数(浮点抽象)上的语义完全不同，并且它并非源自Python的__pow__的实现.

For some particular functions, it may of course be possible to provide a precise encoding to Z3. For example, Z3 supports exponentiation and the Python API provides a __pow__ operator. Note that this operator however, may not have exactly the same semantics as Python's __pow__ on (floating-point abstractions of) real numbers, and it is not derived from Python's implementation of __pow__.

这篇关于z3python:使用数学库的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！