z3 - Translating from Z3Py to SMT-LIB

Question

Please let me know how to translate the following line from Z3Py to SMT-LIB:

def _to_octonion(a):
if isinstance(a, OctonionExpr):
    return a
else:
    return OctonionExpr(a, RealVal(0), RealVal(0), RealVal(0), RealVal(0), RealVal(0), 
                        RealVal(0), RealVal(0))

Many thanks

Answer 1

简短的回答是：做不到。Z3Py 是 Python 之上的 Z3 API（一种为用户提供大量便利的编程语言）。另一方面，SMT-LIB 2.0 是一种公式交换格式，非常有限。SMT-LIB 2.0 文件通常由需要与 SMT 求解器交互的其他程序生成。请注意，上面的函数甚至不会在 SMT-LIB 2.0 格式中“进行类型检查”。输入可以是一个OctonionExpr或“其他任何东西”，输出是一个OctonionExpr（或异常）。