java - 使用 "for all"与未解释的排序 JAVA API

Question

我正在尝试使用 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 表达这个 asserts-foralls 的方式是什么？

Answer 1

Z3 代码中有一组示例，其中包含各种 Java 调用:

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

它们包括构建和检查量化公式。