Этот вопрос является продолжением следующего вопроса.
У меня есть предикат (в данном случае я использую имя «более тяжелый») для двух целых чисел, которые мне нужно оценить с помощью пользовательского алгоритма. Я написал следующий кусок кода, чтобы сделать это. Но я вижу, что параметры, которые передаются в функцию CMTh_reduce_app (), не являются действительными целыми числами, а состоят из типа integer. Мне нужно 2 целых числа, чтобы я мог оценить предикат и вернуть результат (операции, выполняемые в функции CMTh_reduce_app () прямо сейчас, не имеют смысла).
#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);}
Я знаю, что плагин для теории пользователей больше не поддерживается, но мне действительно нужно, чтобы это работало, поэтому, если бы я мог получить какую-либо информацию, это было бы очень полезно. Я пытался взглянуть на исходный код, но я не знал, с чего начать встраивание в него новых теорий. Итак, я был бы признателен за помощь с плагином теории.
Модели не будут доступны для вас из
абстракция, которую предлагает устаревший плагин теории.
Проблема заключается в том, что модели создаются позже в игре.
Это потребовало бы переписывания некоторых внутренних элементов, чтобы приспособить это
(это не невозможно, но очень справедливый кусок работы).
У меня сложилось впечатление, что было бы проще использовать только базовое взаимодействие
с Z3, где вы объявляете предикаты как не интерпретированные, проверьте SAT.
Тогда, если текущие ограничения выполнимы,
использовать текущую модель для оценки аргументов. Если у вас есть ценности, которые противоречат вашему
встроенная процедурная привязанность, затем утверждают новые факты, которые исключают эти значения (и столько же
другие недопустимые значения, насколько это возможно). Я называю это «ленивым циклом».
Эта модель взаимодействия соответствует тому, как SMT-решатели могут использовать
SAT решатели без обеспечения распространения теории (распространение истинных значений
когда новые атомы назначены). Вы должны будете сделать немного больше работы во время
анализ / разрешение конфликтов с целью выработки сильных лемм. Итак, гибрид
между встроенной теорией и подходом ленивых петель может в итоге получиться.
Но прежде чем попасть туда, я предлагаю использовать Z3 как есть и использовать текущую модель для
рассчитать новые блокирующие пункты.
Конечно, вы что-то теряете: создание квантификаторов будет происходить довольно охотно
и вполне может быть так, что этот подход с ленивым циклом не будет работать хорошо в присутствии
квантификаторов.
Других решений пока нет …