在Z3建立自定义理论 [英] Building custom theories in Z3
问题描述
此问题是对以下问题的跟进。
This question is a follow up to the following question.
我有一个谓词（在这种情况下我使用名称重）以使用自定义算法进行评估。我写了下面的代码片段来做。但我看到，传递到函数CMTh_reduce_app（）的参数不是实际的整数，而是整数类型的常量。我需要的是2个整数，所以我可以评估谓词并返回结果（在函数CMTh_reduce_app（）中完成的操作现在是无意义的）。
I have a predicate (I use the name "heavier" in this case) over two integers that I need to evaluate using a custom algorithm. I have written the following piece of code to do it. But I see that the parameters that get passed into the function CMTh_reduce_app() are not actual integers, but consts of type integer. What I need is 2 integers, so that I can evaluate the predicate and return the result (The operations done in the function CMTh_reduce_app() right now are meaningless).
#include<stdio.h>
#include<stdlib.h>
#include<string.h>
#include<stdarg.h>
#include<memory.h>
#include<z3.h>
#include "z3++.h"
#include<iostream>
using namespace z3;
using namespace std;
struct _CMTheoryData {
Z3_func_decl heavier;
};
typedef struct _CMTheoryData CMTheoryData;
Z3_context ctx;
//Exit function
void exitf(const char* message)
{
fprintf(stderr,"BUG: %s.\n", message);
exit(1);
}
//Check and print model if available
void check(Z3_context ctx)
{
Z3_model m = 0;
Z3_lbool result = Z3_check_and_get_model(ctx, &m);
switch (result) {
case Z3_L_FALSE:
printf("unsat\n");
break;
case Z3_L_UNDEF:
printf("unknown\n");
printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
break;
case Z3_L_TRUE:
printf("sat\n%s\n", Z3_model_to_string(ctx, m));
break;
}
if (m) {
Z3_del_model(ctx, m);
}
}
//Create logical context. Enable model generation, and set error handler
void error_handler(Z3_error_code e)
{
printf("Error code: %d\n", e);
exitf("incorrect use of Z3");
}
Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
{
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
ctx = Z3_mk_context(cfg);
#ifdef TRACING
Z3_trace_to_stderr(ctx);
#endif
Z3_set_error_handler(ctx, err);
return ctx;
}
Z3_context mk_context()
{
Z3_config cfg;
Z3_context ctx;
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
return ctx;
}
//Shortcut for binary fn application
Z3_ast mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y)
{
Z3_ast args[2] = {x, y};
return Z3_mk_app(ctx, f, 2, args);
}
//Shortcut to create an int
Z3_ast mk_int(Z3_context ctx, int v)
{
Z3_sort ty = Z3_mk_int_sort(ctx);
return Z3_mk_int(ctx, v, ty);
}
Z3_ast mk_var(Z3_context ctx, const char * name, Z3_sort ty)
{
Z3_symbol s = Z3_mk_string_symbol(ctx, name);
return Z3_mk_const(ctx, s, ty);
}
Z3_ast mk_int_var(Z3_context ctx, const char * name)
{
Z3_sort ty = Z3_mk_int_sort(ctx);
return mk_var(ctx, name, ty);
}
//Callback when final check is to be carried out
Z3_bool CMTh_final_check(Z3_theory t) {
printf("Final check\n");
return Z3_TRUE;
}
//Callback when theory is to be deleted
void CMTh_delete(Z3_theory t) {
CMTheoryData * td = (CMTheoryData *)Z3_theory_get_ext_data(t);
printf("Delete\n");
free(td);
}
//Callback to reduce a function application(definition of custom functions, predicates)
Z3_bool CMTh_reduce_app(Z3_theory t, Z3_func_decl d, unsigned n, Z3_ast const args[], Z3_ast * result) {
CMTheoryData * td = (CMTheoryData*)Z3_theory_get_ext_data(t);
cout<<Z3_ast_to_string(ctx, args[0])<<' '<<Z3_ast_to_string(ctx,args[1])<<endl;
if (d == td->heavier) {
cout<<"Reducing the fn \'heavier\'"<<endl;
if(Z3_is_eq_ast(ctx,mk_int(ctx, 1),args[0])||Z3_is_eq_ast(ctx,mk_int(ctx,2),args[0]))
{
*result = Z3_mk_true(Z3_theory_get_context(t));
return Z3_TRUE;;
}
else
{
*result = Z3_mk_false(Z3_theory_get_context(t));
return Z3_TRUE;;
}
}
return Z3_FALSE; // failed to simplify
}
Z3_theory mk_cm_theory(Z3_context ctx) {
Z3_sort heavier_domain[2];
Z3_symbol heavier_name = Z3_mk_string_symbol(ctx, "heavier");
Z3_sort B = Z3_mk_bool_sort(ctx);
CMTheoryData * td = (CMTheoryData*)malloc(sizeof(CMTheoryData));
Z3_theory Th = Z3_mk_theory(ctx, "cm_th", td);
heavier_domain[0] = Z3_mk_int_sort(ctx);
heavier_domain[1] = Z3_mk_int_sort(ctx);
td->heavier = Z3_theory_mk_func_decl(ctx, Th, heavier_name, 2, heavier_domain, B); //context, theory, name_of_fn, number of arguments, argument type list, return type
Z3_set_delete_callback(Th, CMTh_delete);
Z3_set_reduce_app_callback(Th, CMTh_reduce_app);
Z3_set_final_check_callback(Th, CMTh_final_check);
return Th;
}
main()
{
Z3_ast a_ast, b_ast, c_ast, f1, f3, r;
Z3_sort i;
Z3_pattern p;
Z3_app bound[2];
Z3_theory Th;
CMTheoryData * td;
printf("\nCustom theory example\n");
ctx = mk_context();
Th = mk_cm_theory(ctx);
td = (CMTheoryData*)Z3_theory_get_ext_data(Th);
a_ast = mk_int_var(ctx, "a");
b_ast = mk_int_var(ctx, "b");
bound[0] = (Z3_app)a_ast;
f1=mk_binary_app(ctx, td->heavier, a_ast, b_ast);
r= Z3_mk_exists_const(ctx, 0, 1, bound, 0, 0,f1);
printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, r));
Z3_assert_cnstr(ctx, r);
check(ctx);
}
我知道用户理论插件不是支持，但我真的需要得到这个工作，所以如果我可以得到任何信息，这将是非常有帮助的。我试着查看源代码，但我不知道在哪里开始构建新的理论。
I know the user theory plugin is not supported anymore, but I really need to get this working, so if I could get any information, it would be really helpful. I tried looking at the source code, but I didn't know where to get started with building new theories into it. So, I'd appreciate some help with the theory plugin.
推荐答案
模型不会从
被弃用的理论插件提供的抽象。
问题是，模型在游戏中稍后构建。
这将需要重写一些内部来容纳这个
（这是不可能的，但是一个非常公平的工作）。
Models are not going to be accessible to you from the abstraction that the deprecated theory plugin provides. The problem is going to be that models are constructed later in the game. It would require rewriting some of the internals to accommodate this (it is not impossible, but a very fair chunk of work).
我的印象是，使用只是基本的交互
与Z3更简单，你声明谓词为未解释，检查SAT。
然后如果当前约束是可满足的，
使用当前模型来评估参数。如果你有值，这违背了你的
内置过程附件，然后断言新的事实，规定这些值（和尽可能多的
其他不可行的值）。我称之为惰性循环法。
这个交互模型对应于SMT求解器如何使用
SAT求解器而不提供理论传播（当分配新原子时传播真值值
）。在
冲突分析/解决过程中，你将需要做一些更多的工作，以产生强大的引理。因此，内置理论和延迟循环方法之间的混合
可能最终会解决。
但在到达之前，我建议只使用Z3作为和使用当前模型
计算新的阻塞子句。
当然你失去了一些东西：量词的实例化将进行一些热切的
，这很可能是这种惰性循环方法在量词的存在
不能正常工作的情况。
My impression is that it would be simpler to use just the basic interaction with Z3 where you declare the predicates as uninterpreted, check for SAT. Then if the current constraints are satisfiable, use the current model to evaluate arguments. If you have values, that contradict your built-in procedural attachment, then assert new facts that rule these values out (and as many other infeasible values as possible). I call this the "lazy loop approach". This interaction model corresponds to how SMT solvers can use SAT solvers without providing theory propagation (propagating truth values when new atoms are assigned). You would have to do a bit more work during conflict analysis/resolution in order to produce strong lemmas. So a hybrid between the built-in theory and the lazy loop approach may in the end work out. But before getting there I suggest to just use Z3 as is and use the current model to calculate new blocking clauses. Of course you lose something: instantiation of quantifiers will proceed somewhat eagerly and it could very well be the case that this lazy loop approach will not work well in the presence of quantifiers.
这篇关于在Z3建立自定义理论的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
