如何解决Z3 Java 绑定:为什么在 SMT2 输入文件中设置生产证明会导致错误?
我知道在使用 Z3 的 Java 绑定时,必须在上下文和求解器中启用证明。当输入文件不包含行(set-option :produce-proofs true)
时,以下程序完美运行:
// Setup Context
HashMap<String,String> cfg = new HashMap<String,String>();
cfg.put("proof","true");
Context ctx = new Context(cfg);
// Read input file
BoolExpr[] program = ctx.parseSMTLIB2File(file_name,null,null);
// Create Solver
Solver s = ctx.mkSolver();
s.add(program);
// Set Solver parameters
Params p = ctx.mkParams();
p.add("mbqi",true);
p.add("proof",true);
s.setParameters(p);
// Use Solver
Status status = s.check();
if(status.equals(Status.UNSATISFIABLE)) {
Expr<?> obj = s.getProof();
}
但是,一旦输入文件确实包含行 (set-option :produce-proofs true)
,我就会在执行 parseSMTLIB2File
时收到以下错误消息:
错误设置':produce-proofs',选项值不能修改 初始化”
如果我给定的输入都包含行 (set-option :produce-proofs true)
,那么在 parseSMTLIB2File
期间是否有某种方法可以忽略此行?还是我真的必须相应地修改输入文件?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。