Использование for all с неинтерпретируемыми сортировками JAVA API

Я пытаюсь изучить Z3 с помощью java API, так как нет документации. Я просматривал документацию 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?


java z3 z3py z3c.form
person user3723800    schedule 29.07.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В составе примеров в коде Z3 есть набор примеров с различными вызовами Java:

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

Они включают построение и проверку количественных формул.

person Nikolaj Bjorner    schedule 29.07.2014
comment
Спасибо за ссылку, на самом деле у меня есть эти примеры, но я не нашел в них, как использовать возвращаемое значение функции внутри a for all.. например.. Для выражения (assert(forall((t Task) ) (не (mustPrecede t t)))) Я создаю Expr Task1 = ctx.mkConst(TAKS1,TASK); Expr[] bounds = новое выражение[] { Task1 }; (как показано в примерах), а затем мне нужно создать выражение для тела... но я не знаю, как использовать функцию mustPrece с параметром Task1... не могли бы вы помочь мне с одним примером? - person user3723800; 30.07.2014
comment
Объект FuncDecl имеет функцию Apply, которая принимает набор Expr в качестве аргумента; эти аргументы, конечно, могут быть количественными переменными. Функция quantifierExample2 иллюстрирует использование либо констант (x) в качестве связанных переменных, либо индексированных переменных (mkBound(...)). - person Christoph Wintersteiger; 30.07.2014