z3.prove比求解器更快並且檢查

我正在使用來自Codeplex的最新z3主代碼，標記爲v4.3.1。z3.prove比求解器更快並且檢查

我想要一個像prove這樣的函數，它具有有用的返回值並且不打印。所以，我寫了什麼似乎顯而易見：

def prove2(claim): 
    s = Solver() 
    s.add(Not(claim)) 
    if s.check() == unsat: 
     return True, [] 
    return False, s.model()

然而，這段代碼的運行速度要比默認prove函數慢得多。

在src/api/python/z3.pyprove（瘦身）的代碼是：

def prove(claim, **keywords): 
    s = Solver() 
    s.set(**keywords) 
    s.add(Not(claim)) 
    if keywords.get('show', False): 
     print s 
    r = s.check() 
    if r == unsat: 
     print "proved" 
    elif r == unknown: 
     print "failed to prove" 
     print s.model() 
    else: 
     print "counterexample" 
     print s.model()

當我添加s.set()我的代碼，它是快速和查找相同的反例。

這是怎麼回事？

對s.set()這個空的調用是否清除了某些通常不好的選項？
..對我的特殊測試不好？
還有別的嗎？

我試圖找出什麼是默認的求解器的選擇是，但str(s)repr(s)，s.__dict__，而谷歌並沒有真正的幫助。

任何意見是讚賞！

來源

2014-07-25 Dan Halperin

這是一個有趣的觀察。目前沒有方便的方法來解算器對象的解算器選項。你能否在運行時看到**關鍵字中的內容？ –

嗨@ChristophWintersteiger，因爲我是一個叫'證明（聲明）'的人，我知道**關鍵字是空字典。 –

有趣。你明白什麼「明顯變慢」？你有一個觸發這種行爲的小基準嗎？ –

最好的猜測是默認選項對我的特殊情況做得不好，可能是因爲隨機數差異或其他非確定性內部狀態。

來源

2015-01-02 18:09:33

z3.prove比求解器更快並且檢查

回答

相關問題