seltsames Verhalten beim Überprüfen von Sat Z3

Question

Kann jemand sehen, was ich falsch mache ...Ich verwende den Quantifizierer für alle, um diese beiden Zeilen zu erstellen:

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

das ist der Code..

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

Dann füge ich beides wie folgt zum Löser hinzu:

    // 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")));

aber bei der Behauptung

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

Der Sat-Solver meldet SAT.Dies ist jedoch nicht möglich, da MustePrecede gemäß meinen vorherigen Definitionen mit Quantoren irreflexiv ist.Kann jemand sehen, was mir fehlt oder warum der Sat-Löser die „Einschränkungen“, die ich mit den Foralls hinzugefügt habe, nicht berücksichtigt?

Answer 1

Es gibt zwei Möglichkeiten, quantifizierte Ausdrücke in Z3 zu konstruieren: eine durch die Verwendung benannter Konstanten und die andere durch de-Brujin-indizierte Variablen.Der hier veröffentlichte Code mischt diese beiden und erstellt so Ausdrücke, die sehen richtig, wenn sie es nicht sind.

Die folgenden Teile:

Sort[] tTask = ...
Symbol[] Tnames = ...
...
Expr t1 = ctx.mkConst("t1",Task);
...
Expr mt1t2 = ctx.mkApp(mustPrecede, t1,t2);
...
Expr tra = ctx.mkForall(tTask, Tnames, ...

Konstruieren Sie den Körper des Quantifizierers aus Konstanten („t1“ usw.), aber der Aufruf von ctx.mkForall erfordert de-Brujin-indizierte Variablen (die Indizes sind implizit und). tTask Und tnames weist ihnen Namen zu und sortiert sie).Damit dies funktioniert, muss der Körper mithilfe indizierter Variablen erstellt werden, die durch Aufrufe von generiert werden ctx.mkBound(...).Wenn umgekehrt konstante Ausdrücke bevorzugt werden, könnte der Quantor durch einen Aufruf von erstellt werden ctx.mkForall(Expr[] boundConstants, ... wobei das erste Argument ein Array konstanter Ausdrücke ist, z new Expr[] { t1, t2, t3 }.

Der beste Weg, um zu sehen, warum der Code nicht funktioniert, ist, wenn die Symbole eingefügt werden Tnames werden unterschiedliche Namen zugewiesen.Anhand der Ausgabe ist dann deutlich zu erkennen, dass zwischen diesen Variablen eine Nichtübereinstimmung besteht.Ändern Sie beispielsweise den Code in

....
Expr t1 = ctx.mkConst("x",Task);
Expr t2 = ctx.mkConst("y",Task);
Expr t3 = ctx.mkConst("z",Task);
....

ändert den ersten Quantor in

(forall ((x Task) (y Task) (z Task)) (not (mustPrecede t t)))