如何讓SMT2實例聲明-玩意兒的數量Z3（API）

Question

我用了* Z3_parse_smtlib2_file（C，Z3_string，0,0,0，num_decl，& decl_names，& decls）*嘗試得到變量和變量的數量。但是* num_decl *的值仍然爲零。 我認爲價值將成爲不同的smt2文件。謝謝

Answer 1

參數num_decls,decl_names和decls是輸入參數。它們用於使用C API創建的聲明初始化SMT 2.0解析器符號表。 當前的Z3 API不提供用於提取SMT 2.0格式的文件/字符串中聲明的排序和函數的過程。這些信息在內部提供。請參閱Z3分配src/parsers/smt2和src/cmd_context/cmd_context.*中以下目錄中的文件。