-
Notifications
You must be signed in to change notification settings - Fork 1.6k
Open
Description
Hi there, used Z3 for the first time on a programming Puzzle where i took the Minimize Function to determine the result.
I got some wrong results until i realized it differs if i use "p" as a ConstantName on some special input parameters.
The code should determine the fewest button presses to match some result parameters. A button describes the indices which it affects on the result parameter.
So here i have the sample code where i can reproduce it everytime (with p the result in this case is 277, with another prefix the result is 275):
.NET 10 C# Console Application with Microsoft.Z3 v4.12.2 Nuget Package
using Microsoft.Z3;
List<int[]> buttons = [[2],[0,1,4,6,7],[0,1,8],[1,2,4],[0,3,4,5,8],[0,3,5,6],[2,5],[0,1,4,5,6,7,8],[4],[0,6],[6,8]];
int[] results = [65, 63, 24, 12, 60, 28, 232, 28, 217];
int result = TestZ3(buttons, results, "p"); // switch between p and any other string
Console.WriteLine(result);
int TestZ3(List<int[]> b, int[] r, string constPrefix)
{
using var ctx = new Context();
using var opt = ctx.MkOptimize();
IntExpr[] constants = Enumerable.Range(0, b.Count)
.Select(i => ctx.MkIntConst($"{constPrefix}{i}"))
.ToArray();
foreach (var constant in constants)
opt.Add(ctx.MkGe(constant, ctx.MkInt(0)));
for (int i = 0; i < r.Length; i++)
{
var affecting = constants.Where((_, j) => b[j].Contains(i)).ToArray();
if (affecting.Length > 0)
{
var tmpSum = ctx.MkAdd(affecting);
var boolExpr = ctx.MkEq(tmpSum, ctx.MkInt(r[i]));
opt.Add(boolExpr);
}
}
var handle = opt.MkMinimize(ctx.MkAdd(constants));
opt.Check();
var model = opt.Model;
int sum = 0;
foreach (var constant in constants)
{
int count = ((IntNum)model.Evaluate(constant, true)).Int;
Console.WriteLine(constant + ": " + count);
sum += count;
}
int result = ((IntNum)model.Evaluate(handle.Value, true)).Int;
Console.WriteLine(sum + " " + result);
return result;
}
I hope somebody can confirm my assumption otherwise i hope i will get an explanation for this behavior.
Thanks
Metadata
Metadata
Assignees
Labels
No labels