comportamiento extraño cuando la comprobación se sentó Z3

Question

Puede alguien ver lo que estoy haciendo mal.....Yo estoy usando la de todos los cuantificador para crear estas dos líneas :

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

este es el código..

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

A continuación, voy a añadir tanto para el solver de la siguiente manera:

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

pero al hacer valer

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

El sat solver es la presentación de informes SAT..pero esto si no es posible, ya mustePrecede es irreflexiva de acuerdo a mi definiciones anteriores con cuantificadores..Puede alguien ver lo que me falta o por qué el sat solver no está teniendo en cuenta las "limitaciones" he añadido con el foralls??

Answer 1

Hay dos maneras de construir expresiones cuantificadas en Z3, uno es mediante el uso de constantes con nombre, la otra es de Brujin indexada de variables.El código publicado aquí las mezclas de estos dos y por lo tanto crea las expresiones que buscar a la derecha, cuando no lo son.

De las siguientes partes:

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

construir el cuerpo de la cuantificador de constantes ("t1", etc), pero la llamada a ctx.mkForall requiere de Brujin indexada de variables (los índices están implícitos y tTask y tnames asigna nombres y ordena a ellos).Para que esto funcione, el cuerpo debe ser construido con indexada de variables, que son generados por las llamadas a ctx.mkBound(...).Por el contrario, si la constante de expresiones son los preferidos, el cuantificador podría ser construido por una llamada a ctx.mkForall(Expr[] boundConstants, ... donde el primer argumento es una matriz de constantes expresiones como new Expr[] { t1, t2, t3 }.

La mejor manera de ver la razón de que el código no funciona es cuando los símbolos en Tnames se asignan diferentes nombres.Es entonces claro para ver en la salida que hay una discrepancia entre dichas variables.Por ejemplo, cambiar el código para

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

cambios en el primer cuantificador a

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