我們可以限制Z3中實項的精度嗎？

在我的一個SMT項目中，我使用了一個真正的術語。爲了提高效率，我需要限制實數的精度，因爲對於這個數來說，可能有幾乎無窮多的解，儘管只需要小數點後5/6位。例如，實數的可能估值可以如下，儘管如果我們取小數點後的前七位數字，所有的都是相同的。我們可以限制Z3中實項的精度嗎？

一千三百六十三萬一千四百八十八分之一百一十九萬七千三百二十五= 0.087835238530 ......

218103808分之19157213= 0.087835298134 ......

1744830464分之153257613= 0.087835245980 ......

1226060865/13958643712 = 0.087835243186 ......

我希望SMT解算器將所有這四個數字視爲一個數字（以便搜索空間減少）。有沒有辦法控制實數的精度？

我以編程方式嘗試（使用Z3 Dot Net API）來解決上述問題，如下所示。這裏DelBP [j]是一個真正的術語。

{ 
    BoolExpr[] _Exprs = new BoolExpr[nBuses]; 
    for (j = 1; j <= nBuses; j++) 
    { 
     _Exprs[j - 1] = z3.MkEq(DelBP[j], z3.MkDiv(z3.MkInt2Real(DelBP_A[j]), z3.MkInt2Real(DelBP_B[j]))); 
    } 

    BoolExpr Expr = z3.MkAnd(_Exprs); 
    s.Assert(Expr); 
    tw.WriteLine("(assert {0})", Expr.ToString()); 
} 

{ 
    BoolExpr[] _Exprs = new BoolExpr[nBuses]; 
    for (j = 1; j <= nBuses; j++) 
    { 
     _Exprs[j - 1] = z3.MkAnd(z3.MkGe(DelBP_A[j], z3.MkInt(1)), 
      z3.MkLe(DelBP_A[j], z3.MkInt(10000))); 
    } 

    BoolExpr Expr = z3.MkAnd(_Exprs); 
    s.Assert(Expr); 
    tw.WriteLine("(assert {0})", Expr.ToString()); 
} 

{ 
    BoolExpr[] _Exprs = new BoolExpr[nBuses]; 
    for (j = 1; j <= nBuses; j++) 
    { 
     _Exprs[j - 1] = z3.MkAnd(z3.MkGe(DelBP_B[j], z3.MkInt(1)), 
      z3.MkLe(DelBP_B[j], z3.MkInt(10000))); 
    } 

    BoolExpr Expr = z3.MkAnd(_Exprs); 
    s.Assert(Expr); 
    tw.WriteLine("(assert {0})", Expr.ToString()); 
}

但是，它沒有奏效。任何人都可以幫我解決這個問題嗎？先謝謝你。

來源

2013-08-29 Ashiq

如果您覺得需要控制實數的「精度」，那麼強烈建議Real不是您問題的正確域。一些想法，這取決於你真正想要做的事：

如果6位過去小數點是您所關心的，那麼你可能會使用普通Integer S，由1e6乘以一切，限制脫身所有變量都小於1e6;或其他類似的轉換。
請記住，Z3目前支持IEEE浮點數，這是由精確度有限定義的。所以如果你的域名是IEEE-754規定的浮點數字，那麼你可以使用它們。
如果您試圖生成「連續的」結果，即通過解決問題，然後添加結果應該與前一個不同的約束並再次調用Z3;那麼你可以考慮增加一個約束條件，說明新的結果應該與舊的差別大於絕對值1e6。

這是否適用取決於您正在嘗試解決的具體問題。如果你能分享更多的問題，人們可能會想出其他的想法。但首選應該是搞清楚Real是否真的是你想要使用的域名。

來源

2013-08-29 19:59:12

感謝您的回覆。我不能使用Integer術語，因爲我的實際問題需要浮點值。我已經應用第三種方法來查看通過爲精度添加約束條件可以得到多少不同的結果。但是，我的程序包括第二部分，這取決於這些潛在的價值。我不想將這兩部分分開並以編程方式將它們合併（即在模型外部）。我認爲你的第二個建議可能會起作用。你能提供給我任何鏈接或詳細的建議，可以幫助我更多地瞭解這一點嗎？ – Ashiq

我認爲Z3 Dot Net API不支持IEEE浮點數。可以？ – Ashiq

FP支持相當新穎，如果只有SMT-Lib暫時受支持，這並不會讓我感到意外。但其中一位Z3人需要證實這一點。有關更多信息，請參閱http://stackoverflow.com/questions/15181211/qf-fpa-does-z3-support-ieee-754-arithmetic。 –

我們可以限制Z3中實項的精度嗎？

回答

相關問題