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

Question

Я пытаюсь использовать 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.)

Answer 1

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