题
有人可以看到我做错了什么吗......我使用 for all 量词来创建这两行:
(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))))
这是代码..
Sort User = ctx.mkUninterpretedSort("User");
Sort Task = ctx.mkUninterpretedSort("Task");
//function declaration
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());
//task for using in quatifiers
Expr task = ctx.mkConst("t",Task);
Expr user = ctx.mkConst("u",User);
// creating (assert(forall((t Task)) (not (mustPrecede t t))))
//just one task is needed
Sort[] Tasks = new Sort[1];
Tasks[0] = Task;
//setting the name for the task
Symbol[] namess = new Symbol[1];
namess[0] = ctx.mkSymbol("t");
//Creating a map between mustPrecede and its two parameters
Expr mtt = ctx.mkApp(mustPrecede, task,task);
//acreating not
Expr body = ctx.mkNot((BoolExpr)mtt);
Expr mustPrecedett = ctx.mkForall(Tasks, namess, body, 1, null, null,
ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
System.out.println("Quantifier mustPrecedett: " + mustPrecedett.toString());
//creating (assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1 t2)(mustPrecede t2 t3)) (mustPrecede t1 t3))))
//tree taks will be neede
Sort[] tTask = new Sort[3];
tTask[0] =Task;
tTask[1] =Task;
tTask[2] =Task;
//setting the names for the tasks
Symbol[] Tnames = new Symbol[3];
Tnames[0] = ctx.mkSymbol("t1");
Tnames[1] = ctx.mkSymbol("t2");
Tnames[2] = ctx.mkSymbol("t3");
//creating tree diferent tasks for the relations
Expr t1 = ctx.mkConst("t1",Task);
Expr t2 = ctx.mkConst("t2",Task);
Expr t3 = ctx.mkConst("t3",Task);
//creating mappins
Expr mt1t2 = ctx.mkApp(mustPrecede, t1,t2);
Expr mt2t3 = ctx.mkApp(mustPrecede, t2,t3);
Expr mt1t3 = ctx.mkApp(mustPrecede, t1,t3);
//Creating the relation between them
Expr tbody2= ctx.mkImplies(ctx.mkAnd((BoolExpr)mt1t2,(BoolExpr) mt2t3), (BoolExpr) mt1t3);
//building quatifier
Expr tra = ctx.mkForall(tTask, Tnames, tbody2, 1, null, null,ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
然后我将两者添加到求解器中,如下所示:
// creating (assert(forall((t Task)) (not (mustPrecede t t))))
solver.add(ctx.mkForall(Tasks, namess, body, 1, null, null,ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1")));
//creating (assert(forall((t1 Task)(t2 Task)(t3 Task)) (implies (and (mustPrecede t1 t2)(mustPrecede t2 t3)) (mustPrecede t1 t3))))
solver.add(ctx.mkForall(tTask, Tnames, tbody2, 1, null, null,ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1")));
但当断言
//T2 ; T4 ;(; T12 ; T13 ;AND ; T14 ; T15;) ; T10; T11
Expr T2 = ctx.mkConst("t2", Task);
Expr T3 = ctx.mkConst("t3", Task);
Expr mt = ctx.mkApp(mustPrecede, T2,T3);
Expr mts = ctx.mkApp(mustPrecede, T3,T2);
solver.add(ctx.mkAnd((BoolExpr)mt,(BoolExpr)mts));
sat 解算器正在报告 SAT..但这是不可能的,因为根据我之前对量词的定义,mustePrecede 是非自反的。有人可以看到我缺少什么或者为什么 sat 解算器没有考虑我在 foralls 中添加的“约束”吗?
解决方案
在 Z3 中构造量化表达式有两种方法,一种是使用命名常量,另一种是使用 de-Brujin 索引变量。此处发布的代码混合了这两者,从而创建了表达式 看 是的,当他们不是的时候。
以下部分:
Sort[] tTask = ...
Symbol[] Tnames = ...
...
Expr t1 = ctx.mkConst("t1",Task);
...
Expr mt1t2 = ctx.mkApp(mustPrecede, t1,t2);
...
Expr tra = ctx.mkForall(tTask, Tnames, ...
从常量(“t1”等)构造量词的主体,但是调用 ctx.mkForall
需要 de-Brujin 索引变量(索引是隐式的并且 tTask
和 tnames
为它们分配名称并排序)。为此,需要使用索引变量来构造主体,这些变量是通过调用生成的 ctx.mkBound(...)
。相反,如果首选常量表达式,则可以通过调用来构造量词 ctx.mkForall(Expr[] boundConstants, ...
其中第一个参数是常量表达式数组,例如 new Expr[] { t1, t2, t3 }
.
了解代码为何不起作用的最佳方法是当符号出现时 Tnames
被分配了不同的名称。从输出中可以清楚地看出这些变量之间存在不匹配。例如,将代码更改为
....
Expr t1 = ctx.mkConst("x",Task);
Expr t2 = ctx.mkConst("y",Task);
Expr t3 = ctx.mkConst("z",Task);
....
将第一个量词更改为
(forall ((x Task) (y Task) (z Task)) (not (mustPrecede t t)))
不隶属于 StackOverflow