Z3使用目標和策略

Question

我正在使用Z3和C-API。我想了解如何理解如何在C-API中使用策略和目標。我檢查了Z3的例子，但找不到適合我的例子。

我有我的C-API僞代碼如下 -

contextId = mk_context(); 
solverId = Z3_mk_solver(contextId); 
Z3_solver_inc_ref(contextId, solverId); 
... 
then some assertions like x > 0, y > 0 and so on.. 
... 
// now comes the final goal 
mygoal = Z3_mk_less_than(contextId, ...) // x < 50 
Z3_solver_assert (contextId, solverId, mygoal) 
... 
// finally check 
Z3_solver_check(contextId, solverId) 
Z3_reset_memory(); 
Z3_del_context(contextId); 
Z3_solver_dec_ref(contextId, solverId); 

現在我想一些戰術應用到mygoal。 但是，我無法弄清楚C-API應該如何遵循。 我查了文檔，但找不到這樣的例子。

我試過的是使用Z3_goal_assert(); API。但它不能以某種方式工作。 有人能給我一個C-API的簡單例子嗎？

更新：我嘗試了下面的C代碼，但它不起作用。 在函數調用Z3_tactic_apply()，求解拋出這樣的錯誤 -

pure virtual method called 
terminate called without an active exception 

代碼海賊王：

goalId = Z3_mk_goal();  
Z3_goal_inc_ref(context, goalId); 

assertionVector = Z3_solver_get_assertions (context, solver); 
int vectorSize = Z3_ast_vector_size(assertionVector); 

for(int i=0;i<vectorSize;i++)  
    Z3_goal_assert(context, goalId, Z3_ast_vector_get(context, assertionVector, i)); 

Z3_goal_assert(context, goalId, Z3_mk_eq(context, totalProcDecl, Z3_mk_int(context, numProcessors, int_sort))); 
Z3_goal_assert(context, goalId, Z3_mk_eq(contextlatencyDecl, Z3_mk_int(context, latencyConstraint, int_sort))); 

// This is what I am trying to apply 
// (check-sat-using (then (! simplify :arith-lhs true) solve-eqs lia2pb pb2bv bit-blast sat)) 

tactic0 = Z3_mk_tactic (context, "simplify"); 
Z3_tactic_inc_ref (context,tactic0); 

tactic1 = Z3_mk_tactic (context, "solve-eqs"); 
Z3_tactic_inc_ref (context, tactic1); 

tactic2 = Z3_mk_tactic (context, "lia2pb"); 
Z3_tactic_inc_ref (context, tactic2); 

tactic3 = Z3_mk_tactic (context, "pb2bv"); 
Z3_tactic_inc_ref (context, tactic3); 

tactic4 = Z3_mk_tactic (context, "bit-blast"); 
Z3_tactic_inc_ref (context, tactic4); 

tactic5 = Z3_mk_tactic (context, "sat"); 
Z3_tactic_inc_ref (context, tactic5); 

temp = Z3_tactic_and_then (context, tactic0, tactic1); 
temp = Z3_tactic_and_then (context, temp, tactic2); 
temp = Z3_tactic_and_then (context, temp, tactic3); 
temp = Z3_tactic_and_then (context, temp, tactic4); 
temp = Z3_tactic_and_then (context, temp, tactic5); 

result = Z3_tactic_apply (context, temp, goalId); 
printf("Result : %s\n", Z3_apply_result_to_string (context, result)); 

// Finished Solving. 
Z3_goal_dec_ref (context, goalId); 
Z3_tactic_dec_ref (context, tactic0); 
Z3_tactic_dec_ref (context, tactic1); 
Z3_tactic_dec_ref (context, tactic2); 
Z3_tactic_dec_ref (context, tactic3); 
Z3_tactic_dec_ref (context, tactic4); 
Z3_tactic_dec_ref (context, tactic5); 

我也試着多一個選擇添加參數來簡化策略。

tactic0_without_param = Z3_mk_tactic (context, "simplify"); 
Z3_tactic_inc_ref (context,tactic0_without_param); 

paramsId = Z3_mk_params(context); 
Z3_params_inc_ref(context, paramsId); 
Z3_params_set_bool (context, p, paramsId, Z3_mk_string_symbol(context, ":arith-lhs"), true); 
tactic0 = Z3_tactic_using_params (context, tactic0, paramsId); 

但是再次不起作用。

謝謝。

Answer 1

Z3 4.x帶有C++頭文件，使Z3 C API更易於使用（文件include/z3++.h）。 它也有一個基於C++的示例（文件examples/c++/example.cpp）。這個文件包含許多使用策略對象的例子。

也就是說，戰術應該適用於目標。爲了方便起見，我們還提供了一個API，根據策略Z3_mk_solver_from_tactic創建求解器。該API返回的求解器對象將嘗試使用給定的策略來解決可滿足性查詢。