I am using the .NET API for Z3 and I have discovered strange behaviour (possibly bug in the optimizer) using the code below. When run with the class Optimize, it incorrectly finds a solution, whereas when run with the class Solver, it correctly reports infeasible. Could anyone please run the code to verify my statement? Any hint on what is going on will be highly appreciated.
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;
}
}
}
}
I have tried to reproduce the bug with the current version of the master branch. It reports Infeasible with the Optimize option as well. So the discrepancy between the Solver and Optimize features seems to have been fixed.