2017-06-21 10 views
1

.netと一緒にZ3(バージョン4.5.0.1)を使用したいのですが、SMTLIBファイルを使用できるかどうか疑問です。Microsoft Z3インポートSMTファイル

using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) { 
    context.ParseSMTLIB2String(Resources.SampleSMT2); 
    var solver = context.MkOptimize(); 
    solver.Check(); 
    Console.WriteLine($"model: {solver.Model}"); // empty 
    //BigInteger x = (solver.Model.Evaluate(...) as IntNum).BigInteger; 
    //BigInteger y = (solver.Model.Evaluate(...) as IntNum).BigInteger; 
} 

が、私はで提供問題を解決する方法を知らない:C#で

(declare-const x Int) 
(declare-const y Int) 
(assert (< x 4)) 
(assert (< (- y x) 1)) 
(assert (> y 1)) 

は、私はfolowingをしようと試み: はので、私は私のプログラムにロードするこの単純なSMTファイルを持っていますsmtファイルの場合 この例ではモデルが空です。

答えて

1

ParseSMTLIB2Stringはすなわち、

BoolExpr be = context.ParseSMTLIB2String(...); solver.Add(be); solver.Check(); ...

のようなものがありますを取得する必要があり、SMT2ファイルでアサーションが含まれているBoolExprを返します。

+0

ありがとうございますが、私はそれらを評価できるようにConstInt xとyをどのように取得するのですか? – MrWoffle

+1

あなたは制約を乗り越えてすべてのconstを集める必要があります。類似の質問へのリンクについてはこちらをご覧ください:https://stackoverflow.com/questions/39882992/how-to-get-the-declaration-from-a-z3-smtlib2-formula/40182248#40182248 –

関連する問題