cvc4

    0熱

    1答えて

    CVC4の誘導データ型のアサーション

    私はCVC4で少し実験を試みています。私は次の出力 sat ((x R) (y R)) sat ((x R) (y R)) を取得しています。この使用CVC4を実行すると、私は、この出力により、この動作によって混乱しています (set-option :produce-models true) (set-option :produce-assignments true) (set-lo
    smt algebraic-data-types cvc4 2017-04-22

    0熱

    1答えて

    SMT-LIB 2.6 declare-datatypesステートメントのSMTソルバーのサポート

    SMT-LIBバージョン2.6のdraftは、(declare-datatypes)ステートメントを指定します。この機能のoriginal announcementでは、提案された構文がその時点でZ3とCVC4でサポートされている構文と異なることに言及しています。 現在、SMT-LIB 2.6ドラフトの提案構文をサポートするSMT-LIBサポートを持つSMTソルバー、または提案された構文のサポート
    z3 smt cvc4 2017-03-13

    0熱

    1答えて

    SMT入力用にcvc4のユーザ定義シンボルのオーバーロードを有効にするオプションはありますか？

    1.2からSMT-LIB言語のバージョンでは、ユーザー定義シンボルのオーバーロードが許可されていました。標準のバージョン2.0以降、オーバーロードは理論のシンボルに制限されています。 しかし、SMTソルバーの中には、ユーザー定義のシンボルが過負荷になることがあります。私の使用例では便利です。証拠の義務は、過負荷で自動的に生成されます。 cvc4をSMTソルバーの私のポートフォリオに追加しましたが、
    smt cvc4 2017-08-11

    0熱

    1答えて

    cvc4の実数の対数/指数

    対数や指数を含む実数の式のモデルを提供できるソルバーを探しています。 cvc4は、実数の対数または指数を含む関数を処理できますか？同様に、cvc4は定数eを表現できますか？ this questionによると、Z3は私を助けていない一定の指数を、処理することができます。 This questionは、整数の対数しか問いません。
    logarithm exponent cvc4 2017-11-20

    1熱

    1答えて

    QF_NRAにゼロ除算が含まれていますか？

    ゼロ除算はQF_NRAに含まれていますか？ この問題では、SMT-LIB標準が混乱しています。 paper where the standard is definedでは、この点については説明しません。実際、NRAとQF_NRAはその文書のどこにも表示されません。いくつかの情報はstandard websiteで提供されています。実数は次のように定義されます。 - all terms of the
    z3 smt theorem-proving cvc4 2016-10-21

    1熱

    1答えて

    SMT-LIBのQF_NRAロジックは決定可能ですか？

    SMT-LIBのQF_NRAロジックは決定可能ですか？ 私は、タルスキーが、実数の多項式のシステムが決定可能であるという意味で、非線形演算が決定可能であることを証明したことを知っています。しかし、QF_NRAには分割が含まれているため、QF_NRAがこの傘の下にあることは明らかではありません。最初の質問は、QF_NRAの除算に分母が潜在的にゼロである変数による除算を含むかどうかです。 I post
    z3 smt theorem-proving cvc4 2016-10-21

    1熱

    1答えて

    CVC4：定量化機能を持つboolの機能を合成する設定ですか？私は現在、次の形式の式を解くためにCVC4を使用してい

    ：ここ exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk) 、f1...fnはBoolにBoolのいくつかの数の関数であり、 b1...bkはブール値です。 私の問題は、SMTのUFフラグメントに正当に該当します。それは、量子はありますが、関数とブール値以外のソートはありません。 CVC4
    smt quantifiers cvc4 bounded-quantification 2017-11-26

    1熱

    1答えて

    CVC4の解析エラー（同じ数式がZ3に合格）

    次のSMTフォルマは、CVC4が解析エラーのフラグを立てている間にZ3制約を解決します： "以前に変数として宣言された"私はCVC4 1.4とCVC 1.5の両方をWindows上で使ってテストしました。どのような提案や考え？ (set-logic ALL) (declare-datatypes() ((Enum13 (Green) (Yellow) (None)))) (declare-da
    cvc4 2017-08-22

    1熱

    1答えて

    意味（_ BV0 32）、（_ BV1 16）... SMT2で

    ベンチマークIは、そのいくつかの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_dif
    z3 smt cvc4 2016-09-23
最新の質問