在未解释的排序JAVA API中使用“所有人”

2019-11-21 12:02:04 阅读：257 来源： 互联网

我正在尝试使用Java API学习Z3,因为没有文档,我一直在看C API文档,但是直到现在我仍然找不到如何使用一些基本功能的清晰示例.

我正在尝试编码此Z3代码(在在线版本中有效)

;general options for getting values when sat
(set-option :produce-models true)
(set-option :produce-assignments true)

;declaring new sorts
(declare-sort Task)
(declare-sort User)

;function for assign an specific user
(declare-fun assignUser (Task) User)
;creating a relation between a task and a usert
(declare-fun TaskUser (Task User) Bool)

;stablishing order
(declare-fun mustPrecede (Task Task) Bool)

(assert(forall((t Task)) (not (mustPrecede t t))))
(assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1 t2)(mustPrecede t2 t3)) (mustPrecede t1 t3))))        

;asserting that all task must have one assigned user
(assert(forall((t Task)(u User)) (TaskUser t u)))
;asserting that all task must have one assigned user
;(assert(forall((t1 Task)(t2 Task)) (not(= (assignUser t1) (assignUser t2)))))

到现在为止,我只是设法声明未解释的排序,并按如下方式声明我的函数

      HashMap<String, String> cfg = new HashMap<String, String>();
      cfg.put("proof", "true");
      cfg.put("auto-config", "false");
      Context ctx = new Context(cfg);

    //cfg.put("model", "true");
    Sort USER = ctx.mkUninterpretedSort("USER");
    Sort TASK = ctx.mkUninterpretedSort("TASK");

    FuncDecl assignUser = ctx.mkFuncDecl("assignUser", TASK, USER);
    FuncDecl TaskUser = ctx.mkFuncDecl("TaskUser", new Sort[] { TASK, USER }, ctx.mkBoolSort());
    FuncDecl mustPrecede = ctx.mkFuncDecl("mustPrecede", new Sort[]{TASK,TASK}, ctx.mkBoolSort());

但我找不到表达的例子

(assert(forall((t Task)) (not (mustPrecede t t))))
(assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1 t2) (mustPrecede t2 t3)) (mustPrecede t1 t3))))

;asserting that all task must have one assigned user
(assert(forall((t Task)(u User)) (TaskUser t u)))
;asserting that all task must have one assigned user
;(assert(forall((t1 Task)(t2 Task)) (not(= (assignUser t1) (assignUser t2)))))

有人可以帮我吗？用Java API表示此assert-foralls的方法是什么？

解决方法:

Z3代码中的示例包含一组带有各种Java调用的示例：

https://z3.codeplex.com/SourceControl/latest#examples/java/JavaExample.java

它们包括建立和检查量化公式.

标签：z3py,java,z3,z3c-form
来源： https://codeday.me/bug/20191121/2051764.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

在未解释的排序JAVA API中使用“所有人”