# 2021VMware中国区编程比赛小记

Contents

## 我的方案

《我的团长我的团》——兰晓龙

-module(z3compiler).

-type dna() :: [integer()].
-type method() :: [{StartIndex::integer(), Len::integer()}].
-type direction() :: row | col.
-type matrix() :: [rows()].
-type rows() :: [integer()].
-type ir_exp() :: ir:ir_exp().

-export([gen_ir_code/1]).

-spec compute_dna_for_oneline([integer()]) -> dna().
compute_dna_for_oneline([]) -> [];
compute_dna_for_oneline(L) ->
L1 = lists:dropwhile(fun (I) -> I =:= 0 end, L),
case L1 of
[] ->
[0];
_ ->
L2 = lists:dropwhile(fun (I) -> I =:= 1 end, L1),
Numof1 = length(L1) - length(L2),
case compute_dna_for_oneline(L2) of
[0] ->
[Numof1];
D ->
[Numof1|D]
end
end.

-spec compute_line_from_dna(integer(), integer(), dna()) -> [method()].
compute_line_from_dna(_StartIdx, _EndIdx, []) -> [[]];
compute_line_from_dna(_StartIdx, _EndIdx, [0]) -> [[]];
compute_line_from_dna(StartIdx, EndIdx, [C|DNA]) ->
StartPos = case StartIdx =< EndIdx of
true ->
lists:seq(StartIdx, EndIdx);
false ->
[]
end,
FirstStepChoices = [{I, C}
|| I <- StartPos, I+C-1 =< EndIdx],
lists:append([lists:map(fun (M) -> [{I, L}|M] end,
compute_line_from_dna(I+L+1, EndIdx, DNA))
|| {I, L} <- FirstStepChoices]).

-spec gen_ir_code(matrix()) -> ir_exp().
gen_ir_code(M=[_LL|_]) ->
Mp = transform(M),
ir:make_and_ir([
gen_ir_code_for_lines(M, row),
gen_ir_code_for_lines(Mp, col),
gen_ir_code_not_self(M),
gen_ir_code_range(M)
]).

-spec gen_ir_code_for_line([integer()], integer(), direction()) -> ir_exp().
gen_ir_code_for_line(Line, LineId, Direct) ->
DNA = compute_dna_for_oneline(Line),
Methods = compute_line_from_dna(0, length(Line)-1, DNA),
IRs = [gen_ir_code_for_one_method(Method, LineId, Direct, length(Line))
|| Method <- Methods],
ir:make_or_ir(IRs).

-spec gen_ir_code_for_lines([[integer()]], direction()) -> ir_exp().
gen_ir_code_for_lines(Lines, Direct) ->
IRs = [gen_ir_code_for_line(Line, Id, Direct)
|| {Id, Line} <- lists:zip(lists:seq(0, length(Lines)-1), Lines)],
ir:make_and_ir(IRs).

-spec gen_ir_code_for_one_method(method(), integer(),
direction(), integer()) -> ir_exp().
gen_ir_code_for_one_method(Method, LineId, Direction, Length) ->
Sets = build_set(Method),
R = [{I, case sets:is_element(I, Sets) of
true ->
1;
false ->
0
end}
|| I <- lists:seq(0, Length-1)],
IRs = [case Direction of
row ->
ir:make_eq_ir(LineId, I, V);
col ->
ir:make_eq_ir(I, LineId, V)
end
|| {I, V} <- R],
ir:make_and_ir(IRs).

-spec gen_ir_code_not_self(matrix()) -> ir_exp().
gen_ir_code_not_self(M=[LL|_]) ->
RowIds = lists:seq(0, length(M)-1),
ColIds = lists:seq(0, length(LL)-1),
IRs1 = lists:append([[ir:make_eq_ir(I, J, 0) || {J, Bit} <- lists:zip(ColIds, Line), Bit =:= 1]
|| {I, Line} <- lists:zip(RowIds, M)]),
IRs2 = lists:append([[ir:make_eq_ir(I, J, 1) || {J, Bit} <- lists:zip(ColIds, Line), Bit =:= 0]
|| {I, Line} <- lists:zip(RowIds, M)]),
IRs = case length(IRs1) > length(IRs2) of
true ->
IRs2;
false ->
IRs1
end,
ir:make_or_ir(IRs).

-spec gen_ir_code_range(matrix()) -> ir_exp().
gen_ir_code_range(M=[LL|_]) ->
NRows = length(M),
NCols = length(LL),
ir:make_and_ir(lists:append([[ir:make_ge_ir(I, J, 0), ir:make_le_ir(I, J, 1)]
|| I <- lists:seq(0, NRows-1),
J <- lists:seq(0, NCols-1)]));
gen_ir_code_range(_) -> erlang:error(empty_matrix).

-spec build_set(method()) -> sets:sets(integer()).
build_set(M) ->
S = sets:new(),
build_set(M, S).

build_set([], S) -> S;
build_set([{I, L}|M], S) ->
NewS = sets:union(sets:from_list(lists:seq(I, I+L-1)), S),
build_set(M, NewS).

-spec transform(matrix()) -> matrix().
transform(M=[L|_]) ->
NCols = length(L),
[[lists:nth(R, Rows) || Rows <- M]
|| R <- lists:seq(1, NCols)];
transform(_) -> erlang:error(matrix_empty).


-module(ir).

-type ir_exp() :: {eq, integer(), integer(), integer()}
| {le, integer(), integer(), integer()}
| {ge, integer(), integer(), integer()}
| {'and', [ir_exp()]}
| {'or', [ir_exp()]}.

-export_type([ir_exp/0]).

-export([to_z3/1, to_z3_file/2]).
-export([make_eq_ir/3, make_and_ir/1, make_or_ir/1, make_ge_ir/3, make_le_ir/3]).

-spec make_eq_ir(integer(), integer(), integer()) -> ir_exp().
make_eq_ir(I, J, V) ->
{eq, I, J, V}.

-spec make_and_ir([ir_exp()]) -> ir_exp().
make_and_ir([IR]) -> IR;
make_and_ir(IRs) ->
{'and', IRs}.

-spec make_or_ir([ir_exp()]) -> ir_exp().
make_or_ir([IR]) -> IR;
make_or_ir(IRs) ->
{'or', IRs}.

-spec make_ge_ir(integer(), integer(), integer()) -> ir_exp().
make_ge_ir(I, J, V) ->
{'ge', I, J, V}.

-spec make_le_ir(integer(), integer(), integer()) -> ir_exp().
make_le_ir(I, J, V) ->
{'le', I, J, V}.

-spec to_z3(ir_exp()) -> string().
to_z3({eq, I, J, V}) ->
io_lib:format("(= ~p (A ~p ~p))", [V, I, J]);
to_z3({ge, I, J, V}) ->
io_lib:format("(<= ~p (A ~p ~p))", [V, I, J]);
to_z3({le, I, J, V}) ->
io_lib:format("(>= ~p (A ~p ~p))", [V, I, J]);
to_z3({'and', IRs}) ->
"(and " ++  string:join([to_z3(IR) || IR <- IRs], "\n") ++ ")";
to_z3({'or', IRs}) ->
"(or " ++  string:join([to_z3(IR) || IR <- IRs], "\n") ++ ")".

to_z3_file(IR, File) ->
Head = "(declare-fun A (Int Int) Int)",
Assert = "(assert",
Code = to_z3(IR),
Foot = ")",
Check = "(check-sat)",
S = string:join([Head, Assert, Code, Foot, Check], "\n"),
file:write_file(File, list_to_binary(S)).


Eshell V10.6.4  (abort with ^G)
1> c(z3compiler).
{ok,z3compiler}
2> c(ir).
{ok,ir}
3> Matrix = [[0,1], [1,0]].
[[0,1],[1,0]]
4> IR = z3compiler:gen_ir_code(Matrix).
{'and',[{'and',[{'or',[{'and',[{eq,0,0,1},{eq,0,1,0}]},
{'and',[{eq,0,0,0},{eq,0,1,1}]}]},
{'or',[{'and',[{eq,1,0,1},{eq,1,1,0}]},
{'and',[{eq,1,0,0},{eq,1,1,1}]}]}]},
{'and',[{'or',[{'and',[{eq,0,0,1},{eq,1,0,0}]},
{'and',[{eq,0,0,0},{eq,1,0,1}]}]},
{'or',[{'and',[{eq,0,1,1},{eq,1,1,0}]},
{'and',[{eq,0,1,0},{eq,1,1,1}]}]}]},
{'or',[{eq,0,1,0},{eq,1,0,0}]},
{'and',[{ge,0,0,0},
{le,0,0,1},
{ge,0,1,0},
{le,0,1,1},
{ge,1,0,0},
{le,1,0,1},
{ge,1,1,0},
{le,1,1,1}]}]}
5> ir:to_z3_file(IR, "/tmp/m.z3").
ok


gpadmin@zlyu:~\$ z3 -smt2 /tmp/m.z3
sat
(model
(define-fun A ((x!0 Int) (x!1 Int)) Int
(ite (and (= x!0 0) (= x!1 0)) 1
(ite (and (= x!0 1) (= x!1 1)) 1
0)))
)


## 后记和思考

This site uses Akismet to reduce spam. Learn how your comment data is processed.