Sat Z3을 확인할 때 이상한 동작

Question

누군가 내가 뭘 잘못하고 있는지 볼 수 있습니까?나는 이 두 줄을 만들기 위해 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에 추가한 "제약 조건"을 고려하지 않는지 볼 수 있습니까??

Answer 1

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)))