Microsoft Z3インポートSMTファイル

Question

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

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ファイルの場合 この例ではモデルが空です。

Answer 1

ParseSMTLIB2Stringはすなわち、

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

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