0

我需要使用 jSMTLIB 作为 API。

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

我唯一找到的是不完整的用户指南。（http://www.grammatech.com/resource/smt/jSMTLIBUserGuide.pdf）

任何人都知道在java中创建一个求解器并运行一些断言？

可以给我看一个它是如何工作的例子吗？

谢谢。

4

1 回答 1

0

这是我能做到的：

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

于 2013-07-04T09:38:10.163 回答