CODEWITHSUNDEEP
z3formal-verification
hogeneko
hogeneko

Reputation: 31

Understanding spacer/z3 unsat proof

We use spacer as a backend CHC solver and want to get proof when the result is unsat.

I think that the proof is sufficient to construct a counterexample(a graph reachable to a bad state) but spacer's output is difficult to understand for me. There are some unfamiliar words like asserted or hyper-res.

I couldn't find any document to understand that output. If there is any, please tell me.

I'm really happy if I can construct a counterexample similar to Eldarica's one[0]. For example,

0: FALSE -> 1
1: main_h_30(0, 0, 0, 0, 0, 1, 0, 0, -1, 0, 0, 1) -> 2
2: main_h_28(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 3
3: main_h_24(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 4
4: main_h_22(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 5
5: main_h_21(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 6
6: main_h_18(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 7
7: main_h_16(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 8
8: main_h_13(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 9
9: main_h_11(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 10
10: main_h_9(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 11
11: main_h_8(0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1) -> 12
12: main_h_7(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 13
13: main_h_6(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 14
14: main_h_5(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 15
15: main_h_4(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 16
16: main_h_3(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 17
17: main_h_2(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1) -> 18
18: main_h_1(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1)

[0] http://logicrunch.it.uu.se:4096/~wv/eldarica/?ex=Prolog%2Flistcounter.unsat

Upvotes: 3

Views: 273

Answers (0)

Related Questions