從翻譯到Z3Py SMT-LIB

請讓我知道怎麼翻譯下面一行從Z3Py到SMT-LIB：從翻譯到Z3Py 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))

非常感謝

來源

2013-05-27 Juan Ospina

簡短的回答是：它不能完成。 Z3Py是Python上的Z3 API（一種爲用戶提供了許多便利的編程語言）。另一方面，SMT-LIB 2.0是一種公式交換格式，而且非常有限。 SMT-LIB 2.0文件通常由需要與SMT解算器交互的其他程序生成。請注意，上述功能甚至不會在SMT-LIB 2.0格式中進行「類型檢查」。輸入可以是OctonionExpr或「其他任何」，並且輸出是OctonionExpr（或例外）。

來源

2013-05-27 16:20:27

那麼你的程序複數和其他超複數的擴展只能在Z3Py下工作？ Z3 SMT不可能適應它們？非常感謝 –

我們可以適應，但它不會像Z3Py版本那麼好用。例如，我們將無法重載'+'和'*'等運算符。「自動強制」（例如'_to_octonion'或'_to_complex'）將不會自動應用於我們。例如，'x * x + 2 == 0'是簡潔的寫法，因爲我們使用運算符重載，強制（將'2'轉換爲複雜表達式）等等。 –

我明白了，然後我可以理解它有多美妙Z3Py是。恭喜和非常感謝。 –

從翻譯到Z3Py SMT-LIB

回答

相關問題