Microsoft Z3導入SMT文件

Question

我想使用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(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; 
} 

但我不知道如何解決在提供的問題smt文件，因爲在 這個例子中模型是空的。

Answer 1

ParseSMTLIB2String返回BoolExpr包含在SMT2文件中的說法，即像

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

應該讓你那裏。