cvc4

0熱度

1回答

我在嘗試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

0熱度

1回答

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

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

8熱度

2回答

SMT中量化算術的推理有什麼限制？

我嘗試了好幾種SMT求解器（CVC3，CVC4和Z3）以下看似瑣碎基準： (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall ((x Int)) (forall ((y Int)) (= y x)))) (check-sat) (exit) 求解器都還不得而知。我知道這是一個不可判斷的片段（非線性），但我期待會

1熱度

1回答

如何使用Alt-Ergo執行以下SMT-LIB代碼

以下SMT-LIB代碼在Z3，MathSat和CVC4中運行時沒有問題，但它不在Alt-Ergo中運行，請讓我知道會發生什麼，非常感謝： (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true) (declare-fun m() Bool) (declare-fun p() Bool

1熱度

1回答

CVC4解析錯誤（同一公式通過Z3）

以下SMT葉片通過Z3約束求解，而CVC4標記解析錯誤：「之前聲明爲變量的符號'無'」。我在Windows上測試過使用CVC4 1.4和CVC 1.5。任何建議或想法？ (set-logic ALL) (declare-datatypes() ((Enum13 (Green) (Yellow) (None)))) (declare-datatypes() ((Enum0 (True) (Fal

0熱度

1回答

CVC4期待爲運營商ITE「最多3個參數，發現5

當輸入下列文件cvc4，我得到以下錯誤： (error "Parse Error: <stdin>:11.221: Expecting at most 3 arguments for operator 'ITE', found 5") 文件test.txt是： (declare-fun start!1() Bool) (assert start!1) (declare-fun lt!2

0熱度

1回答

如何使用C++ API在cvc4中旋轉位向量

我嘗試使用C++ API旋轉cvc4中的位向量，但是在涉及到運算符表達式時API有點混亂。使用下面的代碼（摘錄）： #include <iostream> #include <cvc4/cvc4.h> using namespace std; using namespace CVC4; int main() { ExprManager em; SmtEngine

1熱度

1回答

意義（_ BV 0 32），（_ BV1 16）......在SMT2基準測試

我注意到，一些SMT2基準，符號，如(_ bv0 32)，(_ bv16 32)，...，其用途，例如在： QF_FP/schanda /火花/ zeros_consistent_2.smt2 http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev

1熱度

2回答

Z3/cvc4中是否有任何函數可用於計算底數2的對數？

我想證明一個簡化，涉及計算日誌到基地2.是否有任何可用於z3/cvc4計算它的功能？

0熱度

1回答

不能與CVC4ç編譯代碼++ API

我只是想編譯使用g++ helloworld.cpp -lcvc4 -o helloworld -lcvc4 -Wno-deprecated這個文件helloworld.cpp #include <iostream> #include <cvc4/cvc4.h> using namespace CVC4; int main() { ExprManager em; Ex