z3中的符號變量

Question

有沒有辦法讓z3解算器發出「符號」解決方案？例如，對於等式：

1 + X = C

的解是x = C-1，但總是Z3發射特定模型，如[c = 0, x = -1]。如何將c定義爲符號變量？

Answer 1

不幸的是，Z3沒有公開這種功能。雖然我們在內部使用解算器，但它們不在API中公開。在未來的版本中，我們希望公開內部組件，例如：求解器，Grobner基礎程序等。在當前版本中，我們有一個叫做solve-eqs（見http://rise4fun.com/Z3Py/tutorial/strategies）的策略。它使用高斯消元的泛化來消除變量。但是，這是一個預處理步驟，您無法控制哪些變量被消除。