在Z3 .NET API中優化會導致錯誤的結果 - bug？

Question

我正在使用Z3的.NET API，並且使用下面的代碼發現了奇怪的行爲（可能是優化器中的錯誤）。與類Optimize一起運行時，它不正確地找到解決方案，而與類Solver一起運行時，它正確地報告不可行。任何人都可以運行代碼來驗證我的聲明？任何有關正在發生的事情的提示都將受到高度讚賞。

親切的問候

馬立克

using System; 
using System.Collections.Generic; 
using Microsoft.Z3; 

namespace DS 
{ 
    class Program 
    { 
     static void Main(string[] args) 
     { 
      SMTtest smt = new SMTtest(); 
      if (smt.Solve()) 
      { 
       Console.WriteLine("Solved"); 
      } 
      else 
      { 
       Console.WriteLine("Infeasible"); 
      } 
     } 
    } 

    class SMTtest 
    { 
     public bool Solve() 
     { 
      using (Context ctx = new Context(new Dictionary<string, string>() { { "model", "true" } })) 
      { 
       Optimize optimizer = ctx.MkOptimize(); 
       //Solver optimizer = ctx.MkSolver(); 

       int numOfTasks = 19; 
       IntExpr[] time = new IntExpr[numOfTasks * 2]; 
       BoolExpr[] select = new BoolExpr[numOfTasks]; 

       for (int i = 0; i < numOfTasks; i++) 
       { 
        select[i] = ctx.MkBoolConst("valid" + i.ToString()); 
       } 
       for (int i = 0; i < numOfTasks * 2; i++) 
       { 
        time[i] = ctx.MkIntConst("time" + i.ToString()); 
       } 

       optimizer.Assert(ctx.MkEq(select[1], select[0])); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[1]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[20]))); 
       optimizer.Assert(ctx.MkEq(select[8], select[0])); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[8]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[27]))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[0], time[1]), ctx.MkEq(time[0], time[8])))); 
       optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[19], time[20]), ctx.MkEq(time[19], time[27])))); 
       optimizer.Assert(ctx.MkEq(select[2], select[1])); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[2]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[21]))); 
       optimizer.Assert(ctx.MkEq(select[5], select[1])); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[5]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[24]))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[1], time[2]), ctx.MkEq(time[1], time[5])))); 
       optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[20], time[21]), ctx.MkEq(time[20], time[24])))); 
       optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[2], time[3]))); 
       optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[21], time[22]))); 
       optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[2], time[4]))); 
       optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[21], time[23]))); 
       optimizer.Assert(ctx.MkEq(select[2], ctx.MkOr(select[3], select[4]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[3], select[4] }, 1)); 
       optimizer.Assert(select[3]); 
       optimizer.Assert(ctx.MkEq(time[3], ctx.MkInt(0))); 
       optimizer.Assert(ctx.MkEq(time[22], ctx.MkInt(4))); 
       optimizer.Assert(ctx.MkNot(select[4])); 
       optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[5], time[6]))); 
       optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[24], time[25]))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[5], time[7]))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[24], time[26]))); 
       optimizer.Assert(ctx.MkEq(select[5], ctx.MkOr(select[6], select[7]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[6], select[7] }, 1)); 
       optimizer.Assert(select[6]); 
       optimizer.Assert(ctx.MkEq(time[6], ctx.MkInt(0))); 
       optimizer.Assert(ctx.MkEq(time[25], ctx.MkInt(1))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkGe(time[7], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[26], ctx.MkAdd(time[7], ctx.MkInt(1))))); 
       optimizer.Assert(ctx.MkEq(select[9], select[8])); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[9]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[28]))); 
       optimizer.Assert(ctx.MkEq(select[12], select[8])); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[12]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[31]))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[8], time[9]), ctx.MkEq(time[8], time[12])))); 
       optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[27], time[28]), ctx.MkEq(time[27], time[31])))); 
       optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[9], time[10]))); 
       optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[28], time[29]))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[9], time[11]))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[28], time[30]))); 
       optimizer.Assert(ctx.MkEq(select[9], ctx.MkOr(select[10], select[11]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[10], select[11] }, 1)); 
       optimizer.Assert(ctx.MkNot(select[10])); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkGe(time[11], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[30], ctx.MkAdd(time[11], ctx.MkInt(14))))); 
       optimizer.Assert(ctx.MkEq(select[13], select[12])); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[13]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[32]))); 
       optimizer.Assert(ctx.MkEq(select[16], select[12])); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[16]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[35]))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[12], time[13]), ctx.MkEq(time[12], time[16])))); 
       optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[31], time[32]), ctx.MkEq(time[31], time[35])))); 
       optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[13], time[14]))); 
       optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[32], time[33]))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[13], time[15]))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[32], time[34]))); 
       optimizer.Assert(ctx.MkEq(select[13], ctx.MkOr(select[14], select[15]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[14], select[15] }, 1)); 
       optimizer.Assert(select[14]); 
       optimizer.Assert(ctx.MkEq(time[14], ctx.MkInt(1))); 
       optimizer.Assert(ctx.MkEq(time[33], ctx.MkInt(5))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkGe(time[15], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[34], ctx.MkAdd(time[15], ctx.MkInt(11))))); 
       optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[16], time[17]))); 
       optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[35], time[36]))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[16], time[18]))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[35], time[37]))); 
       optimizer.Assert(ctx.MkEq(select[16], ctx.MkOr(select[17], select[18]))); 
       optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[17], select[18] }, 1)); 
       optimizer.Assert(ctx.MkNot(select[17])); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkGe(time[18], ctx.MkInt(7)))); 
       optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[37], ctx.MkAdd(time[18], ctx.MkInt(12))))); 
       optimizer.Assert(select[0]); 

       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[5], select[8]), ctx.MkLe(ctx.MkSub(time[8], time[5]), ctx.MkInt(0)))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[8], select[5]), ctx.MkLe(ctx.MkSub(time[5], time[8]), ctx.MkInt(0)))); 

       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[7]), ctx.MkOr(ctx.MkGe(time[3], time[26]), ctx.MkGe(time[7], time[22])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[15]), ctx.MkOr(ctx.MkGe(time[3], time[34]), ctx.MkGe(time[15], time[22])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[10]), ctx.MkOr(ctx.MkGe(time[4], time[29]), ctx.MkGe(time[10], time[23])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[17]), ctx.MkOr(ctx.MkGe(time[4], time[36]), ctx.MkGe(time[17], time[23])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[11]), ctx.MkOr(ctx.MkGe(time[6], time[30]), ctx.MkGe(time[11], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[14]), ctx.MkOr(ctx.MkGe(time[6], time[33]), ctx.MkGe(time[14], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[18]), ctx.MkOr(ctx.MkGe(time[6], time[37]), ctx.MkGe(time[18], time[25])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[7], select[15]), ctx.MkOr(ctx.MkGe(time[7], time[34]), ctx.MkGe(time[15], time[26])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[10], select[17]), ctx.MkOr(ctx.MkGe(time[10], time[36]), ctx.MkGe(time[17], time[29])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[14]), ctx.MkOr(ctx.MkGe(time[11], time[33]), ctx.MkGe(time[14], time[30])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[18]), ctx.MkOr(ctx.MkGe(time[11], time[37]), ctx.MkGe(time[18], time[30])))); 
       optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[14], select[18]), ctx.MkOr(ctx.MkGe(time[14], time[37]), ctx.MkGe(time[18], time[33])))); 


       if (optimizer.Check() == Status.SATISFIABLE) 
       { 
        ctx.Dispose(); 
        return true; 
       } 
       ctx.Dispose(); 
       return false; 
      } 
     } 
    } 
} 

Answer 1

我試圖重現bug與主分支的最新版本。它也報告了優化選項不可行。所以Solver和Optimize功能之間的差異似乎已經修復。