Commit df3be842 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Tests: annotate dynamic_constraints

parent 42c57f9f
......@@ -656,26 +656,53 @@ def init_forward_unfolding_solution_1(mcla):
# Shift of the system clauses and auxiliary clauses is made now.
expected = [
# [_lit0, _h2] [_lit0, D] [_h2, D, _lit0] [P, _lit5] [L, _lit5] [P, L, _lit5]
[[-24, 16], [-24, 4], [-16, -4, 24], [-15, 42], [-12, 42], [15, 12, -42],
# [_lit5, _lit4] [K, _lit4] [_lit5, K, _lit4] [B, _lit3] [_lit4, _lit3] [B, _lit4, _lit3]
[-42, 41], [-11, 41], [42, 11, -41], [2, -40], [41, -40], [-2, -41, 40],
# [_lit3, _lit2] [M, _lit2] [_lit3, M, _lit2] [A, _lit1] [_lit2, _lit1] [A, _lit2, _lit1]
[40, -36], [-13, -36], [-40, 13, 36], [1, -25], [36, -25], [-1, -36, 25],
[-43, 22], [-43, 25], [-22, -25, 43], [-47, 24, 1], [-47, 24, -43],
[47, -24], [47, -1, 43], [5, -44], [6, -44], [-5, -6, 44], [-45, 17],
[-45, 44], [-17, -44, 45], [1, -27], [41, -27], [-1, -41, 27], [27, -26],
[-13, -26], [-27, 13, 26], [2, -46], [26, -46], [-2, -26, 46], [-30, 22],
[-30, 46], [-22, -46, 30], [-48, 45, 2], [-48, 45, -30], [48, -45],
[48, -2, 30], [31, -30], [31, -43], [30, 43, -31], [-49, 31, 3], [49, -31],
[49, -3], [-50, 4], [-50, -24], [50, -4, 24], [-51, 5], [-51, -45],
[51, -5, 45], [-52, 6], [52, -6], [-32, 21], [-32, 7], [-21, -7, 32],
# [_lit6, _h_0] [_lit6, _lit1] [_h_0, _lit1, _lit6]
[-43, 22], [-43, 25], [-22, -25, 43],
# [A, _lit0, A] [A, _lit0, _lit6] [A, _lit0] [A, A, _lit6]
[-47, 24, 1], [-47, 24, -43], [47, -24], [47, -1, 43],
# [E, _lit7] [F, _lit7] [E, F, _lit7] [_lit8, _h3] [_lit8, _lit7] [_h3, _lit7, _lit8]
[5, -44], [6, -44], [-5, -6, 44], [-45, 17], [-45, 44], [-17, -44, 45],
# [A, _lit11] [_lit4, _lit11] [A, _lit4, _lit11] [_lit11, _lit10] [M, _lit10] [_lit11, M, _lit10]
[1, -27], [41, -27], [-1, -41, 27], [27, -26], [-13, -26], [-27, 13, 26],
# [B, _lit9] [_lit10, _lit9] [B, _lit10, _lit9] [_lit14, _h_0] [_lit14, _lit9] [_h_0, _lit9, _lit14]
[2, -46], [26, -46], [-2, -26, 46], [-30, 22], [-30, 46], [-22, -46, 30],
# [B, _lit8, B] [B, _lit8, _lit14] [B, _lit8] [B, B, _lit14]
[-48, 45, 2], [-48, 45, -30], [48, -45], [48, -2, 30],
# [_lit15, _lit14] [_lit15, _lit6] [_lit14, _lit6, _lit15] [C, _lit15, C] [C, _lit15] [C, C]
[31, -30], [31, -43], [30, 43, -31], [-49, 31, 3], [49, -31], [49, -3],
# [D, D] [D, _lit0] [D, D, _lit0] [E, E] [E, _lit8] [E, E, _lit8]
[-50, 4], [-50, -24], [50, -4, 24], [-51, 5], [-51, -45], [51, -5, 45],
# [F, F] [F, F] [_lit16, _h7] [_lit16, G] [_h7, G, _lit16]
[-52, 6], [52, -6], [-32, 21], [-32, 7], [-21, -7, 32],
# [G, G] [G, _lit16] [G, G, _lit16] [H, _lit16, H] [H, _lit16] [H, H]
[-53, 7], [-53, -32], [53, -7, 32], [-54, 32, 8], [54, -32], [54, -8],
# [_lit17, _h6] [_lit17, K] [_h6, K, _lit17] [_lit18, _h4] [_lit18, I] [_h4, I, _lit18]
[-33, 20], [-33, 11], [-20, -11, 33], [-34, 18], [-34, 9], [-18, -9, 34],
[-55, 33, 9], [-55, 33, -34], [55, -33], [55, -9, 34], [-35, 19], [-35, 10],
[-19, -10, 35], [-56, 34, 10], [-56, 34, -35], [56, -34], [56, -10, 35],
[-57, 35, 11], [-57, 35, -33], [57, -35], [57, -11, 33], [-58, 12],
[58, -12], [-37, 23], [-37, 14], [-23, -14, 37], [-38, 23], [-38, 14],
[-23, -14, 38], [39, -37], [39, -38], [37, 38, -39], [-60, 14], [-60, -39],
[60, -14, 39], [-59, 37, 13], [59, -37], [59, -13], [-61, 38, 15], [61, -38],
[61, -15], [-18, 9], [-19, 10], [-20, 11], [-21, 7], [-16, 4], [-17, 5],
# [I, _lit17, I] [I, _lit17, _lit18] [I, _lit17] [I, I, _lit18]
[-55, 33, 9], [-55, 33, -34], [55, -33], [55, -9, 34],
# [_lit19, _h5] [_lit19, J] [_h5, J, _lit19]
[-35, 19], [-35, 10], [-19, -10, 35],
# [J, _lit18, J] [J, _lit18, _lit19] [J, _lit18] [J, J, _lit19]
[-56, 34, 10], [-56, 34, -35], [56, -34], [56, -10, 35],
# [K, _lit19, K] [K, _lit19, _lit17] [K, _lit19] [K, K, _lit17]
[-57, 35, 11], [-57, 35, -33], [57, -35], [57, -11, 33],
# [L, L] [L, L] [_lit20, _h_1] [_lit20, N] [_h_1, N, _lit20]
[-58, 12], [58, -12], [-37, 23], [-37, 14], [-23, -14, 37],
# [_lit21, _h_1] [_lit21, N] [_h_1, N, _lit21] [_lit22, _lit20] [_lit22, _lit21] [_lit20, _lit21, _lit22]
[-38, 23], [-38, 14], [-23, -14, 38], [39, -37], [39, -38], [37, 38, -39],
# [N, N] [N, _lit22] [N, N, _lit22] [M, _lit20, M] [M, _lit20] [M, M]
[-60, 14], [-60, -39], [60, -14, 39], [-59, 37, 13], [59, -37], [59, -13],
# [P, _lit21, P] [P, _lit21] [P, P]
[-61, 38, 15], [61, -38], [61, -15],
# [_h4, I] [_h5, J] [_h6, K] [_h7, G] [_h2, D] [_h3, E]
[-18, 9], [-19, 10], [-20, 11], [-21, 7], [-16, 4], [-17, 5],
# [_h_0, A, B] [_h_1, N, N]
[-22, 1, 2], [-23, 14, 14]]]
# Crap
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment