uses z3;

fn main
[
	var lines := list_break_to_lines(read_lazy(h[0]));
	var sum := 0;
	for l in lines do [
		var m := list_break_whitespace(l);
		var buttons := empty(int);
		for i := 1 to len(m) - 1 do [
			var s := m[i][1 .. len(m[i]) - 1];
			var n := map(list_break(s, ','), ston);
			var b := 0;
			for j := 0 to len(n) do
				b bts= n[j];
			buttons +<= b;
		]
		var jolt := empty(int);
		var mm := m[len(m) - 1];
		var s := mm[1 .. len(mm) - 1];
		var n := map(list_break(s, ','), ston);

		implicit var z3w := z3_mk_world;
		var ctx := z3_mk_context();

		var min_str := "(minimize (+";
		for i := 0 to len(buttons) do [
			z3_eval_smtlib2_string_noret(ctx, "(declare-const button-"+ntos(i)+" Int)");
			z3_eval_smtlib2_string_noret(ctx, "(assert (>= button-"+ntos(i)+" 0))");
			min_str += " button-"+ntos(i);
		]
		min_str += "))";
		z3_eval_smtlib2_string_noret(ctx, min_str);
		for i := 0 to len(n) do [
			var str := "(assert (= "+ntos(n[i])+"(+ 0";
			for j := 0 to len(buttons) do [
				if buttons[j] bt i then
					str += " button-"+ntos(j);
			]
			str += ")))";
			z3_eval_smtlib2_string_noret(ctx, str);
		]
		var sat := z3_eval_smtlib2_string(ctx, "(check-sat)");
		if not list_begins_with(sat, "sat") then
			abort;
		var model := z3_eval_smtlib2_string(ctx, "(get-model)");
		var model_lines := list_break_to_lines(model);
		for m in model_lines do [
			if list_begins_with(m, "    ") then
				sum += ston(m[4 .. len(m) - 1]);
		]
	]
	write(h[1], ntos(sum) + nl);
]