search

private-yusuke / smt-d

A small SMT solver implementation for QF_UF and LRA[WIP]. 2021年度の情報特別演習Iにて書いたプログラム
MIT License
1 stars 0 forks source link

QF_UF の merge が嘘ではないか #4

Closed private-yusuke closed 2 years ago

private-yusuke commented 2 years ago

https://github.com/private-yusuke/smt-d/blob/1a71570fdd65487137ba4e08353544a96ebef1a8/source/theory_solver/qf_uf_solver.d#L340

ここでは P_u \times P_v について foreach ループを回したいので、https://dlang.org/phobos/std_algorithm_setops.html#cartesianProduct を使うべき

foreach (p; cartesianProduct(getPredecessors(u), getPredecessors(v)))

で直るかな