Использование z3 api для решения LRA работает медленнее, чем использование z3 в терминале

Я пытаюсь использовать Z3 для решения случайной обобщенной задачи упаковки полос (LRA) и вызываю Z3 api в программе c, вот код.

Z3_context ctx;
Z3_ast fs;
LOG_MSG("smt2parser_example");
FILE *fp = fopen("smttest","r");  
if(fp == NULL)  
{
    perror("fopen()");
    return;
}
int file_size;
fseek(fp,0,SEEK_END);
file_size = ftell( fp );

char *tmp;
fseek( fp , 0 , SEEK_SET);
tmp =  (char *)malloc( (file_size+1) * sizeof( char ) );
tmp[file_size]='\0';
fread( tmp , file_size , sizeof(char) , fp);

ctx = mk_context();
fs  = Z3_parse_smtlib2_string(ctx, tmp, 0, 0, 0, 0, 0, 0);
Z3_assert_cnstr(ctx, fs);

Z3_model m      = 0;

Z3_check(ctx);

Z3_del_context(ctx);

Я также пытаюсь решить smttest в терминале командой «z3 smttest». Однако в терминале он работает быстрее, чем вызов api в программе c. Интересно, есть ли какая-либо конфигурация, которую мне нужно установить, чтобы она работала быстро в режиме API? (Кстати, z3 работает в терминале в два раза быстрее, чем вызов API.)


c z3 smt
person Yinrun    schedule 22.09.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Функция "Z3_assert_cnstr(ctx, fs);" больше не доступен, поэтому вы должны использовать очень старую версию Z3. Используйте объекты «решателя» для утверждения выражений, а также используйте C++ API для повышения надежности. Вы можете создавать решатели для определенной логики, например "QF_LRA", и в этом случае первоначальная настройка принудительно соответствует этой логике. По умолчанию Z3 попытается автоматически найти хорошие настройки, проанализировав заявленные формулы перед первой проверкой.

person Nikolaj Bjorner    schedule 22.09.2016
comment
Большое спасибо за ваш ответ. Я создаю решатель для логики QF_LRA, и эта проблема была решена. - person Yinrun; 22.09.2016