2

我正在使用带有 C-API 的 Z3。我试图了解如何理解如何在 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);

现在我想对我的目标应用一些策略。但是，我无法了解 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);

但再次不起作用。

谢谢。

4

1 回答 1

4

Z3 4.x 带有 C++ 头文件，使 Z3 C API 更易于使用（文件include/z3++.h）。它还有一个基于 C++（文件examples/c++/example.cpp）的示例。该文件包含许多使用策略对象的示例。

话虽如此，策略应该应用于目标。为方便起见，我们还提供了一个 API，可以从 tactic 创建求解器Z3_mk_solver_from_tactic。此 API 返回的求解器对象将尝试使用给定的策略解决可满足性查询。

于 2012-09-17T17:30:39.247 回答