comportement étrange lors de la vérification de sat Z3

Question

Quelqu'un peut-il voir ce que je fais de mal....Je suis à l'aide de la pour tous les quantificateurs pour créer ces deux lignes :

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

c'est le 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"));

Ensuite, je suis d'ajouter les deux à la solveur comme suit:

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

mais lorsqu'il fait valoir

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

Le sat solver est de déclaration SAT..mais ce n'es pas possible, car mustePrecede est irreflexive selon mes définitions précédentes avec des quantificateurs..Quelqu'un peut-il voir ce que je suis absent ou pourquoi le sat solver est de ne pas considérer les "contraintes" j'ai ajouté avec le foralls??

Answer 1

Il y a deux façons de construire des expressions quantifiées dans Z3, un seul est par l'utilisation nommé constantes, l'autre est par de Brujin indexé variables.Le code posté ici mélanges de ces deux et crée ainsi des expressions qui look droit, quand ils ne le sont pas.

Les parties suivantes:

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

construire le corps du quantificateur de constantes ("t1", etc), mais l'appel à la ctx.mkForall nécessite de Brujin indexé variables (les indices sont implicites et tTask et tnames assigne des noms et des tris à eux).Pour que cela fonctionne, le corps a besoin d'être construit à l'aide de variables indexés, qui sont générés par des appels à ctx.mkBound(...).A l'inverse, si des expressions constantes sont privilégiées, le quantificateur pourraient être construits par un appel à ctx.mkForall(Expr[] boundConstants, ... où le premier argument est un tableau d'expressions constantes comme new Expr[] { t1, t2, t3 }.

La meilleure façon de voir pourquoi le code ne fonctionne pas, c'est quand les symboles dans Tnames sont attribués des noms différents.Il est alors facile de voir à partir de la sortie qu'il existe une incompatibilité entre ces variables.Par exemple, en modifiant le code de

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

changements le premier quantificateur à

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