smt

1熱度

1回答

我目前正在嘗試使用Z3爲具有多態列表的無類型語言編碼簡單程序邏輯。據我所知，從the Z3 tutorial by Moura and Bjorner，不可能「嵌套在其他類型，如數組內的遞歸數據類型定義」。因此，假設我有以下OCaml的類型： type value = | Num of float | String of string | List of valu

1熱度

1回答

Z3精度爲實數和小數值

Z3中Real變量的通常精度是多少？是否使用了精確算術？有沒有辦法手動設置精度等級？如果Real意味着必須使用精確算術，那麼對於精度有限的浮點值是否還有其他數據類型？最後：從這個角度來看，z3與其他流行的SMT解算器有什麼不同，還是這種標準化的SMT-LIB定義？

1熱度

1回答

Microsoft Z3導入SMT文件

我想使用Z3（版本4.5.0.1）.net，並想知道我是否可以使用SMTLIB文件。所以我有我想在我的程序加載這個簡單的SMT文件： (declare-const x Int) (declare-const y Int) (assert (< x 4)) (assert (< (- y x) 1)) (assert (> y 1)) 在C＃中我tryed如下因素： using(Con

0熱度

1回答

有沒有一種選項可以在cvc4中爲SMT輸入重載用戶定義的符號？

在SMT-LIB語言的1.2到1.2版本中，允許用戶定義符號的重載。自標準2.0版以來，超載僅限於理論符號。儘管如此，一些SMT解決者仍然允許重載用戶定義的符號，這對我的用例來說很方便：證明義務很容易通過重載自動生成，而不是沒有...我想添加cvc4添加到我的SMT解決方案組合中，但是我發現它會在重載的用戶符號上產生解析錯誤。我知道這是符合SMT-LIB標準的正確方法，但我想知道以下內容：是否有

2熱度

1回答

Z3中的部分定義

我試圖在Z3中定義成對關係（在下面的代碼中稱爲C）（使用數組定義）之間的parthood關係。我寫了3個斷言來定義反身性，傳遞性和反對稱性，但Z3返回「未知」，我不明白爲什麼。 (define-sort Set() (Array Int Bool)) (declare-rel C (Set Set)) ; reflexivity (assert (forall ((X Set)) (C

-2熱度

1回答

在Z3中如何「最小化」工作

我在Z3中使用最小化函數很多，我擔心一些可伸縮性問題（當我最小化變量的數量增長時）。「最小化」的底層算法是什麼？有沒有一種通用的方法來加快速度？

3熱度

2回答

是否有可能在Z3中檢測到不一致的方程式，或者在傳遞給Z3之前？

我正在用以下示例使用z3。 f=Function('f',IntSort(),IntSort()) n=Int('n') c=Int('c') s=Solver() s.add(c>=0) s.add(f(0)==0) s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c)))) 最後的等式是不一致的（因爲n=c將使其不確定）。但是

1熱度

1回答

無法爲z3py提取Z3 EnumSort的值

我正在嘗試將問題編碼到Z3中，並且我希望爲「三態」布爾值（即，帶有true,false和unknown的布爾值）建模。這裏是我怎麼也仿照它： #!/usr/bin/env python import z3 from collections import OrderedDict TristateValues = ["True", "False", "Unknown"] Tristate

4熱度

1回答

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

是否有增量式SMT解算器或某些增量式SMT解算器的API，我可以在其中增量添加約束，我可以通過某些標籤/名稱唯一標識每個約束？我想唯一標識約束的原因是我可以稍後通過指定該標籤/名稱來放棄它們。需要放棄約束是因爲我早先的約束與時間無關。我看到，與Z3我不能使用基於推/彈出的增量方法，因爲它遵循基於堆棧的想法，而我的要求是放棄特定的早期/舊約束。隨着Z3基於假設的其他增量方法，我將不得不執行格

0熱度

1回答

關於CVC4中的歸納數據類型的斷言

我在嘗試CVC4的實驗。 (set-option :produce-models true) (set-option :produce-assignments true) (set-logic QF_UFDT) (declare-datatypes() (Color (Red) (Black)) ) (declare-const x C) (declare-const y C