سلوك غريب عند فحص جلس 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..لكن هذا غير ممكن لأن mustePrecede غير انعكاسي وفقًا لتعريفاتي السابقة مع محددات الكمية..هل يمكن لأي شخص أن يرى ما أفتقده أو لماذا لا يأخذ مُحلل الجلوس بعين الاعتبار "القيود" التي أضفتها مع الشكل؟؟

Answer 1

هناك طريقتان لإنشاء تعبيرات كمية في Z3، إحداهما باستخدام الثوابت المسماة، والأخرى باستخدام متغيرات دي بروجين المفهرسة.يمزج الكود المنشور هنا بين هذين الاثنين وبالتالي ينشئ تعبيرات ينظر صحيح، عندما لا يكونون كذلك.

الأجزاء التالية:

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