Z3在執行過程中添加新變量

Question

我正在嘗試向Z3添加新功能。 此功能要求我在執行期間和預處理後添加新的鬆弛變量。 我找不到合適的方法，我擔心試圖通過添加一個新列強制它會「破壞」解算器。

有沒有一種常見的推薦方式來做到這一點？

感謝， 奧馬爾

Answer 1

您可以將文件src/smt/theory_arith_int.h中找到一個例子，方法：mk_gomory_cut。 在此方法的最後，創建了一個新的多項式約束，並將其存儲在變量bound中。然後，下面的代碼段是用來「內化」的約束：

literal l  = null_literal; 
    context & ctx = get_context(); 
    ctx.internalize(bound, true); 
    l = ctx.get_literal(bound); 

方法internalize將回調theory_arith，和一個新的鬆弛被創建。 備註：方法internalize假設存儲在bound中的多項式約束是簡化形式。