0

以前の提案によると、z3Py の使用中にソルバーの早期タイムアウトを設定しようとしています。

繰り返しますが、すべての詳細なしで、これは私が試みていることです:

for bits in range(A, B, incrmt)
    s = Solver();
    s.set("timeout", 30) #30, 3000, 30000, 60000 no change
    s.add(some constraints)
    if(s.check() == sat):
        print "Sat, %d," %(bits)
    else:
        print "Sat Unknown, %d," %(bits)
        break
    sys.stdout.flush()

基本的に、タイムアウトは発生しません (ミリ秒単位の非常に短い時間であっても)。

4

1 に答える 1

1

LinuxまたはFreeBSDでZ3を使用していますか？これらのプラットフォームのタイマーに関連するバグがありました。問題を修正しましたが、まだ公式リリースには含まれていません。詳細については、次の投稿を参照してください。

于 2013-02-06T05:58:29.460 に答える