z3py

    0熱度

    2回答

    Unsatisfiable公式？也許錯誤的語法？

    公式，我想解決這個樣子的在C： #define foo(w,x,y) ((((w)*(x)*(y)+31) & ~31)/8) WORD w,x,y,z; y = 24; if((foo(w,x,y) * z) == -1) printf("yeah!"); 我把它改寫以下列方式來z3py： from z3 import * w= BitVec('w',16) x= Bit
    z3 smt z3py 2014-02-13

    5熱度

    3回答

    我在哪裏可以獲得z3py教程

    rise4fun由於一些安全問題，z3py在幾周內不可用。我試圖找出一些學習z3py的資源，但是徒然結束。請建議一些資源來學習z3py
    z3 z3py 2013-11-15

    0熱度

    1回答

    Z3py是否支持線性時間邏輯LTL？

    Z3py支持線性時間邏輯LTL嗎？ 如果是，你能提供一個簡單解釋的例子。
    z3 constraint-programming z3py 2013-11-15

    2熱度

    1回答

    如何設置z3py中的核心數

    根據http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html我可以在z3命令行中設置CC_NUM_THREADS = 4，如果我使用的是.smt文件。 如果我使用z3py api，該怎麼做？
    z3 z3py 2014-02-27

    2熱度

    1回答

    如何定義矩陣？

    它看起來像微軟完全pooched他們的「rise4fun」網站和Z3 Python tutorial不再加載。 如何定義在Z3中爲Python定義矩陣並對其施加一些約束？
    python z3 z3py 2014-01-11

    1熱度

    1回答

    如何在Ubuntu上使用Z3運行smtLib文件？

    例如，我有一個smtLib文件'encoding.smt'。現在我想在z3上運行這個文件（standalone exe），在Ubuntu機器上給定超時和內存分配。像： $./z3 encoding.smt 240(sec) 6(GB) 我已經從Z3下載頁面下載了ubuntu 32位zip文件。我現在要做什麼？ 'bin'文件夾中有一個z3應用程序。我需要更改任何環境變量 - 如果我想在Ubun
    z3 z3py 2013-11-27

    2熱度

    1回答

    或位矢量z3Py

    理想情況下，可能'或'兩個數字表示爲位矢量，但我不能夠。請告訴我們，如果沒有在代碼中的一些錯誤或別的東西 line1 = BitVec('line1', 1) line2 = BitVec('line2', 1) s = Solver() s.add(Or(line1, line2) == 0) print s.check() 給出的錯誤是 error: 'type error' W
    python z3 smt z3py bitvector 2014-03-12

    3熱度

    2回答

    Z3無法在羣論中證明權利取消的屬性？

    我想證明一些在羣論中的一般性質。 例如左取消屬性：（XY = XZ）=>（Y = Z）它證明用下面的代碼 (declare-sort S) (declare-fun e() S) (declare-fun mult (S S) S) (declare-fun inv (S) S) (assert (forall ((x S) (y S) (z S)) (= (mult (mult x y)
    z3 z3py 2014-01-23

    5熱度

    2回答

    如何將Z3py和Sympy一起使用

    我想對矩陣執行一些符號計算（將符號作爲矩陣的條目），然後我會有一些可能的解決方案。我的目標是根據約束選擇解決方案/解決方案。 例如，M是具有一個元素作爲symbol的矩陣。 這個矩陣將有2個特徵值，一個是正數，一個是負數。使用z3我試圖找出只有負值，但我無法這樣做，因爲一個被定義爲一個符號，我不能把它寫成一個約束，除非我將它轉換爲一個實際值。 我該怎麼辦？有沒有什麼辦法，以在轉換（符號）不動產或整
    python z3 sympy z3py 2014-03-18

    4熱度

    1回答

    如何z3py表達式轉換爲smtlib 2格式

    我的問題是關於：Z3: convert Z3py expression to SMT-LIB2? 我想z3py從表達到smtlib2格式轉換。使用下面的腳本，但是轉換後，當我喂結果Z3或任何其他SMT，我得到： 「語法錯誤，意外讓」 有什麼辦法，我可以帶它使用z3py在smtlib2格式，以便我不必再次寫長表達式。 下面是我使用的轉換代碼： def convertor(f, status="unk
    python python-2.7 z3 z3py 2014-03-24
最新問題