strange behavior when checking sat Z3

Question

Can somebody see what I am doing wrong.... I am using the for all quantifier to create this two lines :

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

this is the 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"));

Then I am adding both to the solver as follows:

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

but when asserting

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

The sat solver is reporting SAT.. but this si not possible since mustePrecede is irreflexive according to my previous definitions with quantifiers.. Can somebody see what I am missing or why the sat solver is not considering the "constraints" I added with the foralls??

Answer 1

There are two ways to construct quantified expressions in Z3, one is by using named constants, the other is by de-Brujin indexed variables. The code posted here mixes these two and thus creates expressions that look right, when they aren't.

The following parts:

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

construct the body of the quantifier from constants ("t1" etc), but the call to ctx.mkForall requires de-Brujin indexed variables (the indexes are implicit and tTask and tnames assigns names and sorts to them). For this to work, the body needs to be constructed using indexed variables, which are generated by calls to ctx.mkBound(...). Conversely, if constant expressions are preferred, the quantifier could be constructed by a call to ctx.mkForall(Expr[] boundConstants, ... where the first argument is an array of constant expressions like new Expr[] { t1, t2, t3 }.

The best way to see why the code doesn't work is when the symbols in Tnames are assigned different names. It is then plain to see from in output that there is a mismatch between those variables. For example, changing the code to

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

changes the first quantifier to

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