使用z3 api來解決LRA運行速度比在終端中使用z3慢

Question

我想用Z3解決一個隨機的廣義帶包裝問題（LRA），我在c程序中調用Z3 api，這裏是代碼。

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); 

我也嘗試通過命令「z3 smttest」解決終端中的smttest問題。但是，在終端中，它運行速度比在c程序中調用api快。我想知道是否有任何配置需要設置，以便在api模式下運行得更快（順便說一下，z3在終端運行速度比調用api快兩倍）。

Answer 1

函數「Z3_assert_cnstr（ctx，fs） ;」已不再可用，因此您必須使用Z3的舊版本。使用「求解器」對象來斷言表達式，並使用C++ API來提高可靠性。您可以爲指定的邏輯創建解算器，例如「QF_LRA」，在這種情況下，初始設置必須適合該邏輯。默認情況下，Z3會嘗試通過在第一次檢查之前分析斷言的公式來自動找到好的設置。