這個表情真的不好嗎？

我調試我的代碼，然後我遇到了Z3說，這表達不飽和度這個表情真的不好嗎？

(and (not (>= s 13)) 
    (>= s 0) 
    (>= 13 s) 
    (>= pc0_thread1 0) 
    (>= pc1_thread1 0) 
    (>= pc2_thread1 0) 
    (>= pc3_thread1 0) 
    (>= pc4_thread1 0) 
    (>= pc0_main 0) 
    (>= pc0_thread2 0) 
    (>= pc1_thread2 0) 
    (= 1 pc0_main))

我很驚訝，並試圖使用unsat_core功能，但它返回一個空數組。我錯過了什麼嗎？

來源

2014-02-28 Zeinab Ganjei

我的錯誤是我在一個循環中使用了「解算器」，但是我沒有每次都重置，所以它有來自以前循環迭代的信息，從而產生錯誤的結果。打印solver.assertions（）後，我想清楚發生了什麼！

謝謝大家。

來源

2014-03-04 09:46:22

我獲得「坐」

(declare-fun s() Real) 
(declare-fun pc0_thread1() Real) 
(declare-fun pc1_thread1() Real) 
(declare-fun pc2_thread1() Real) 
(declare-fun pc3_thread1() Real) 
(declare-fun pc4_thread1() Real) 
(declare-fun pc0_main() Real) 
(declare-fun pc0_thread2() Real) 
(declare-fun pc1_thread2() Real) 
(assert (and (not (>= s 13)) 
(>= s 0) 
(>= 13 s) 
(>= pc0_thread1 0) 
(>= pc1_thread1 0) 
(>= pc2_thread1 0) 
(>= pc3_thread1 0) 
(>= pc4_thread1 0) 
(>= pc0_main 0) 
(>= pc0_thread2 0) 
(>= pc1_thread2 0) 
(= 1 pc0_main)))

（檢查-SAT）

運行這個例子在線here

來源

2014-02-28 11:03:05

像胡安，我得到SAT，但我已經對整數試過：

(declare-const s Int) 
(declare-const pc0_thread1 Int) 
(declare-const pc1_thread1 Int) 
(declare-const pc2_thread1 Int) 
(declare-const pc3_thread1 Int) 
(declare-const pc4_thread1 Int) 
(declare-const pc0_main Int) 
(declare-const pc0_thread2 Int) 
(declare-const pc1_thread2 Int) 

(assert (and (not (>= s 13)) 
    (>= s 0) 
    (>= 13 s) 
    (>= pc0_thread1 0) 
    (>= pc1_thread1 0) 
    (>= pc2_thread1 0) 
    (>= pc3_thread1 0) 
    (>= pc4_thread1 0) 
    (>= pc0_main 0) 
    (>= pc0_thread2 0) 
    (>= pc1_thread2 0) 
    (= 1 pc0_main)) 
) 

(check-sat)

Zeinab：我認爲你不使用SMT2前端，而是使用API。你能給我們提供更多關於你在用這個表達方式做什麼的信息嗎？例如，我們最近有一個關於ctx-solver-simplicity策略的錯誤報告，提供了錯誤的結果（請參閱here），但我必須確切知道您的目標是什麼樣的，以及您正在應用的策略。

來源

2014-02-28 11:08:22

這個表情真的不好嗎？

回答

相關問題