如何在Z3中實現自定義簡化策略？

在我的工具中，我使用將常量與整數變量進行比較的條件（例如y < 100）。通常，對於一個變量有多種條件，我想簡化這些情況。例如：y & y！= 99應該變成y < 99.簡化策略不會這樣做，並且沒有任何簡化聲音的參數可以幫助他們。如何在Z3中實現自定義簡化策略？

代碼：

context c; 
goal g(c); 
expr x = c.int_const("x"); 
expr y = c.int_const("y"); 
solver s(c); 
expr F = y < 100 && y != 99; 
g.add(F); 
tactic t = tactic(c, "simplify"); 
apply_result r = t(g); 
for (unsigned i = 0; i < r.size(); i++) { 
    std::cout << "subgoal " << i << "\n" << r[i] << "\n"; 
}

到底返回輸出：subgoal 0 (goal (not (<= 100 y)) (not (= y 99)))

，而不是subgoal 0(goal(not(<= 99 y))或類似的，我希望它是什麼。

因此我想實現我自己的簡化策略。不幸的是我找不到如何做到這一點。我知道，這個策略需要在C++中實現，但是我怎樣才能將我的策略引入Z3？

來源

2014-01-21 Niels Thole

Z3策略存儲在目錄中：src/tactic。算術相關策略位於子目錄arith中。你應該使用現有的策略作爲實施策略的「模板」。一個很好的例子是 https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

爲了使API和SMT 2.0前端中提供的新戰術，我們必須包括含有ADD_TACTIC命令的註釋。該命令指示Z3 mk_make腳本將所有內容粘合在一起。參數是：策略的名稱，描述和創建策略的C++代碼。

/* 
    ADD_TACTIC("normalize-bounds", 
      "replace a variable x with lower bound k <= x with x' = x - k.", 
      "mk_normalize_bounds_tactic(m, p)") 
*/

順便說一句，你還可以通過擴展現有的策略，如實施新的功能： https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp

來源

2014-01-22 05:29:19

如何在Z3中實現自定義簡化策略？

回答

相關問題