Z3：使用Java API簡化斷言

我在Windows 7以及Java 7 64位上使用Z3版本4.3.2的Java-API 64位。Z3：使用Java API簡化斷言

我試圖使用簡化來獲得有關我的斷言集合中冗餘信息的知識。

我的第一次嘗試是簡化布爾表達式和評估這樣

Expr e = ctx.mkImplies(ctx.mkBoolConst("A"),ctx.mkBoolConst("B")).simplify();

結果在我的例子

(=> A B)    
(=> (not B) C) 
(=> A B) 
(=> B A) 
(=> D E) 
(=> B F) 
(=> G D) 
(=> H I) 
(=> I (not D)) 
(=> (not D) I) 
(=> C (not B)) 
C)

這導致簡化的公式

(and 
    (or (not A) B) 
    or B C) 
    or (not B) A) 
    (or (not D) E) 
    (or (not B) F) 
    (or (not G) D) 
    (or (not H) I) 
    (or (not I) (not D)) 
    (or D I) 
    (or (not C) (not B)) 
    C 
)

我在爲了將它們簡化爲一個表達式，之前將這些含義包含在AND表達式中。

這個結果還不是我想要的。原始代碼第三行中的重複規則被取出（這很好）。但是，如果C爲真（示例的最後一行），則B必須爲假（(=> C (not B))）。如果B爲假，則A必須爲假（(=> A B)）。等等...

我expexted什麼更像以下（我這樣做手工，因此轉換可能有誤差）

(and 
    (or (not A) B)  ; transformed to (not A) 
    or B C)    ; transformed to C 
    or (not B) A)  ; deleted 
    (or (not D) E)  ; left unchanged 
    (or (not B) F)  ; deleted 
    (or (not G) D)  ; left unchanged 
    (or (not H) I)  ; left unchanged 
    (or (not I) (not D)) ; left unchanged 
    (or D I)    ; left unchanged 
    (or (not C) (not B)) ; transformed to (not B) 
    C     ; C 
)

接下來，我嘗試使用的戰術像下面

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify"); 
Tactic smtTactic = ctx.mkTactic("smt"); 
Tactic then = ctx.then(simplifyTactic, smtTactic, new Tactic[] {}); 
Solver solver = ctx.mkSolver(then); 
solver.add(bel2.toArray(new BoolExpr[0])); // bel2 is List<BoolExpr> 
Status status = solver.check();

這樣做會導致模型而不是簡化。此外，對於我來說，簡化策略是可行的，對我來說有點困難。通常結果是未知的，原因「不完整」。

我上面描述的預期結果是否可以用Z3進行計算？如何做呢？

我環顧四周在這個論壇了，但我的觀點是不是真的回答...

來源

2014-02-07 John Smith

作爲一種策略，在smt一個不會導致在你試圖斷言的任何改造或簡化實現，這是可滿足性的策略，所以對於某些斷言，它會返回sat，不可知，或者可能超時。

使用簡化策略更符合您的需求，但您可能需要應用不同的策略才能實現所需的轉換。然而，當我在SMT-LIB格式編碼的問題，並使用ctx-solver-simplify戰術爲你想，它返回我認爲你在尋找什麼（rise4fun鏈接：http://rise4fun.com/Z3/r2id）：

(declare-fun A() Bool) 
(declare-fun B() Bool) 
(declare-fun C() Bool) 
(declare-fun D() Bool) 
(declare-fun E() Bool) 
(declare-fun F() Bool) 
(declare-fun G() Bool) 
(declare-fun H() Bool) 
(declare-fun I() Bool) 

(assert (and (=> A B)    
(=> (not B) C) 
(=> A B) 
(=> B A) 
(=> D E) 
(=> B F) 
(=> G D) 
(=> H I) 
(=> I (not D)) 
(=> (not D) I) 
(=> C (not B)) 
C)) 

(apply ctx-solver-simplify) 
; result: 
; (goals 
; (goal 
; (=> A B) 
; (or (not D) E) 
; (or (not G) D) 
; (or (not H) I) 
; (or (not I) (not D)) 
; (or D I) 
; (not B) 
; C 
; :precision precise :depth 1) 
;)

爲了您的實驗中，您可能需要審查策略（http://rise4fun.com/z3/tutorialcontent/strategies#h21），並在使用API之前嘗試一些SMT-LIB接口，因爲實驗可能會更快。另外，如你所見，這會返回一個目標。在Java API，請嘗試更改爲以下並查看ApplyResult對象的Subgoals場（是Goal對象的集合），看它是否有你想要的東西：

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify"); 
Goal g = ctx.mkGoal(); 
g.Assert(bel2.toArray(new BoolExpr[0])); 
ApplyResult a = simplifyTactic.Apply(g); 
// look at a.Subgoals

這是基於我的經驗在.NET API，它可以從Java一個略有不同，但你可以檢查出Goal Java文檔在這裏： https://z3.codeplex.com/SourceControl/changeset/view/8bfbdf1e680d#src/api/java/Goal.java

來源

2014-02-07 16:16:14 Taylor

只是要小心，似乎有當前是一個問題，CTX-求解器簡化，請參閱http： //z3.codeplex.com/workitem/95 –

Z3：使用Java API簡化斷言

回答

相關問題