z3 - Z3 の実数項の精度を制限できますか?

Question

私の SMT プログラムの 1 つで、実数を使用しています。小数点以下 5/6 桁のみが必要ですが、この数値にはほぼ無限の数の解が可能であるため、効率を上げるために実数の精度を制限する必要があります。たとえば、実数の可能な評価は次のようになりますが、小数点以下の最初の 7 桁を取る場合はすべて同じです。

1197325/13631488 = 0.087835238530......

19157213/218103808 = 0.087835298134......

153257613/1744830464 = 0.087835245980......

1226060865/13958643712 = 0.087835243186......

SMT ソルバーがこれら 4 つの数値をすべて 1 つの数値と見なすようにします (検索スペースを減らすため)。実数の精度を制御する方法はありますか?

以下に示すように、上記の問題をプログラムで (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());
}

しかし、うまくいきませんでした。誰でもこの問題を解決するのを手伝ってもらえますか? 前もって感謝します。