增量式SMT解算器具有降低特定約束的能力

Question

是否有增量式SMT解算器或某些增量式SMT解算器的API，我可以在其中增量添加約束，我可以通過某些標籤/名稱唯一標識每個約束？

我想唯一標識約束的原因是我可以稍後通過指定該標籤/名稱來放棄它們。 需要放棄約束是因爲我早先的約束與時間無關。 我看到，與Z3我不能使用基於推/彈出的增量方法，因爲它遵循基於堆棧的想法，而我的要求是放棄特定的早期/舊約束。 隨着Z3基於假設的其他增量方法，我將不得不執行格式爲「（check-sat p1 p2 p3）」的check-sat，即如果我有三個斷言來檢查，那麼我將需要三個布爾常量p1， p2，p3，但在我的實現中，我會一次檢查數千個斷言，間接需要數千個布爾常量。 我還檢查了JavaSMT，一個用於SMT求解器的Java API，以查看API是否提供了一些更好的方法來處理這個需求，但我發現只有通過「addConstraint」或「push」添加約束並且無法找到任何方法的方法刪除或刪除特定約束，因爲pop是唯一可用的選項。

我想知道是否有任何增量解算器可以添加或刪除由名稱唯一標識的約束，或者是有其他方式處理它的API。我會很感激任何建議或意見。

Answer 1

基於「堆棧」的方法基本上是根深蒂固到SMTLib中的，所以我認爲找到一個完全符合你想要的算法是很困難的。雖然我同意這將是一個很好的功能。

話雖如此，我可以想出兩個解決方案。但是，兩者都不能很好地服務於你的特定用例，儘管它們都將工作。事實上，您希望能夠在每次致電check-sat時挑選自己的約束條件。不幸的是，這將是昂貴的。每當求解器做出check-sat時，它就會根據所有當前斷言學到很多引理，並且相應地修改了很多內部數據結構。基於堆棧的方法基本上允許解算器「回溯」到其中一種學習狀態。但是，當然，這不允許你觀察櫻桃採摘。

所以，我認爲你留下了下列之一：

使用check-SAT-假設

這主要是你已經描述了。但要回顧一下，不要斷言布爾人，而只是給他們起個名字。所以，這樣的：

(assert complicated_expression) 

成爲

; for each constraint ci, do this: 
    (declare-const ci Bool) 
    (assert (= ci complicated_expression)) 
    ; then, check with whatever subset you want 
    (check-sat-assuming (ci cj ck..)) 

這會增加你必須管理布爾常量的數量，但在某種意義上，這些都是「名」你要進不去。我知道你不喜歡這個，因爲它引入了很多變數;事實確實如此。這有一個很好的理由。看到這個討論在這裏：https://github.com/Z3Prover/z3/issues/1048

使用復位斷言和：全球聲明

這是允許在每次調用check-sat你隨意摘櫻桃的斷言變種。但它會不是便宜。特別是，求解器會在你每次遵循這個配方時忘記它學到的所有東西。但它會做你想要的。第一個問題：

(set-option :global-declarations true) 

並以某種方式跟蹤所有這些你自己在你的包裝。現在，如果你想任意「添加」一個約束，你不需要做任何事情。只需添加它。如果你想刪除的東西，那麼你說：

(reset-assertions) 
(assert your-tracked-assertion-1) 
(assert your-tracked-assertion-2) 
;(assert your-tracked-assertion-3) <-- Note the comment, we're skipping 
(assert your-tracked-assertion-4) 
..etc 

等。也就是說，你「刪除」你不想要的。請注意，調用:global-declarations非常重要，因爲它會確保您在調用reset-assertions時確保您的所有數據聲明和其他綁定保持完整，這會告訴求解器從一開始就學到的東西開始。

實際上，您正在管理自己的約束，正如您首先想要的那樣。

摘要

這些解決方案無論是正是你想要的東西，但他們會工作。沒有采用這兩種解決方案中的任何一種，根本就沒有SMTLib兼容的方式來做你想做的事情。然而，個人解決方案可能會有其他的技巧。您可能想要與他們的開發人員覈對，看看他們是否可以爲這個用例定製一些東西。雖然我懷疑是這樣，但很高興找到！

也看到尼古拉此以前的答案是非常相關的：How incremental solving works in Z3?