jSMTLIB作爲API

Question

我需要使用jSMTLIB作爲API。

但我找不到任何可以幫助我的教程。

我發現的唯一的事情是用戶指南不完整。 （http://www.grammatech.com/resource/smt/jSMTLIBUserGuide.pdf）

任何人都知道在java中創建求解器並運行一些斷言？

能告訴我一個它如何工作的例子嗎？

謝謝。

Answer 1

這是據我可以去：

public class MySMT extends SMT{ 

    public static void main(String[] args){  
    MySMT msm = new MySMT(); 

    Script sc; 
    try { 
     sc = msm.createScript();  
     msm.solver = msm.startSolver(msm.smtConfig, 
           msm.property("org.smtlib.defaultSolver"), 
           msm.property("org.smtlib.solver_simplify") 
    ); 

     IResponse resp = sc.execute(msm.solver); 
     msm.printScript(sc); 
    } catch (Exception e) { 
     e.printStackTrace(); 
    } 
    } 


    public MySMT(){ 
    super(); 
    this.props = this.readProperties();  
    } 

    public String property(String key){ 
    return this.props.getProperty(key); 
    } 

    public Script createScript() throws IOException{ 
    List<ISort> argSorts = new LinkedList<ISort>(); 

    SMTExpr.Symbol logicSymbol = new SMTExpr.Symbol("AUFLIA"); 
    C_set_logic logic = new C_set_logic(logicSymbol); 

    SMTExpr.Symbol sym = new SMTExpr.Symbol("a-boolean-function"); 
    C_declare_fun declar = new C_declare_fun(sym,argSorts, Sort.Bool()); 

    C_assert assertion = new C_assert(sym);   
    C_check_sat cksat = new C_check_sat(); 

    List<IExpr> args = new LinkedList<IExpr>(); 
    args.add(sym); 
    args.add(new SMTExpr.Symbol("false")); 
    C_assert newassertion = new C_assert(
     new SMTExpr.FcnExpr(new SMTExpr.Symbol("="),args) 
     ); 

    C_get_model gmods = new C_get_model(); 

    Script sc = new Script(null,null);  
    sc.add(logic); 
    sc.add(declar); 
    sc.add(assertion); 
    sc.add(cksat); 
    //sc.add(newassertion); 
    sc.add(cksat); 
    // get-model does not work on Simplify 
    //sc.add(gmods); 

    return sc; 
    } 

    public void printScript(Script sc) throws Exception{ 
    OutputStreamWriter osw = new OutputStreamWriter(System.out); 
    Printer pr = new Printer(osw); 
    sc.accept(pr); 
    osw.close(); 
    } 

    public class MyConfig extends SMT.Configuration{ 

    } 

} 

如果你的目標是編程的方式創建一個SMT腳本並執行它： 參見上面的createScript功能，以及如何將其打印文件使用printScript中的模式。然後，您可以通過創建一個Process並使用它來執行jSMTLIB。

問題用jSMTLIB：如果我嘗試以編程方式調用一個腳本文件的程序循環抱怨解析器發現了一個「EOD字符」命令行。 （utf 0019，媒體結束）。爲避免這種情況，您必須將腳本放在一對括號之間。有趣的是，來自shell的命令行不會因此而受到影響。 在這兩種情況下，雖然(get-model) SMT指令不被接受。

如果你的目標是使用jSMTLIB執行命令逐步 它的工作原理部分：

簡化 - 工程;

Z3 - 最新版本不適合我。

我認爲這與Simplify是互動的事實有關，但Z3不是。 因此，在上面的代碼中，當使用Z3時，您將獲得IOException，因爲當jSMTLIB嘗試訪問它們時，流向Z3進程的流將關閉。

請確保正確放置屬性文件。閱讀（不完整）教程，看看在哪裏放置包含這些屬性和鍵的屬性文件，例如我上面寫的org.smtlib.defaultSolver。

你也可以傳遞額外的參數在屬性文件中求解： org.smtlib.solver_<name-of-the-solver>.command=<arguments-to-the-solver>

不幸的是我不能用的參數要麼打讓Z3工作。 無論如何，如果你想使用Z3，也爲它的Java API，它應該提供幾乎相同的功能jSMTLIB應該有：

http://research.microsoft.com/en-us/um/people/leonardo/blog/2012/12/10/z3-for-java.html