1 (*----------------------------------------------*) |
1 (*----------------------------------------------*) |
2 (* Reorder clauses for use in binary resolution *) |
2 (* Reorder clauses for use in binary resolution *) |
3 (*----------------------------------------------*) |
3 (*----------------------------------------------*) |
4 |
4 |
5 fun drop n [] = [] |
|
6 | drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) |
|
7 |
|
8 fun remove_nth n [] = [] |
5 fun remove_nth n [] = [] |
9 | remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n)) |
6 | remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n)) |
10 |
7 |
11 fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) |
8 (*Differs from List.nth: it counts from 1 rather than from 0*) |
|
9 fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs)) |
12 |
10 |
13 |
11 |
14 exception Not_in_list; |
12 exception Not_in_list; |
15 |
13 |
16 |
|
17 fun zip xs [] = [] |
|
18 | zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys)) |
|
19 |
|
20 |
|
21 fun unzip [] = ([],[]) |
|
22 | unzip((x,y)::pairs) = |
|
23 let val (xs,ys) = unzip pairs |
|
24 in (x::xs, y::ys) end; |
|
25 |
14 |
26 fun numlist 0 = [] |
15 fun numlist 0 = [] |
27 | numlist n = (numlist (n - 1))@[n] |
16 | numlist n = (numlist (n - 1))@[n] |
28 |
17 |
29 |
18 |
36 |
25 |
37 fun minus a b = b - a; |
26 fun minus a b = b - a; |
38 |
27 |
39 |
28 |
40 (* code to rearrange clauses so that they're the same as the parsed in SPASS version *) |
29 (* code to rearrange clauses so that they're the same as the parsed in SPASS version *) |
41 |
|
42 fun assoc3 a [] = raise Recon_Base.Noassoc |
|
43 | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t; |
|
44 |
|
45 |
|
46 fun third (a,b,c) = c; |
|
47 |
|
48 |
30 |
49 fun takeUntil ch [] res = (res, []) |
31 fun takeUntil ch [] res = (res, []) |
50 | takeUntil ch (x::xs) res = if x = ch |
32 | takeUntil ch (x::xs) res = if x = ch |
51 then |
33 then |
52 (res, xs) |
34 (res, xs) |
68 |
50 |
69 fun get_eq_strs str = if eq_not_neq str (*not an inequality *) |
51 fun get_eq_strs str = if eq_not_neq str (*not an inequality *) |
70 then |
52 then |
71 let val (left, right) = takeUntil "=" str [] |
53 let val (left, right) = takeUntil "=" str [] |
72 in |
54 in |
73 ((butlast left), (drop 1 right)) |
55 (butlast left, tl right) |
74 end |
56 end |
75 else (* is an inequality *) |
57 else (* is an inequality *) |
76 let val (left, right) = takeUntil "~" str [] |
58 let val (left, right) = takeUntil "~" str [] |
77 in |
59 in |
78 ((butlast left), (drop 2 right)) |
60 (butlast left, tl (tl right)) |
79 end |
61 end |
80 |
62 |
81 |
63 |
82 |
64 |
83 fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a |
65 fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a |
99 falselist = [] |
81 falselist = [] |
100 end |
82 end |
101 |
83 |
102 |
84 |
103 |
85 |
104 fun var_pos_eq vars x y = let val xs = explode x |
86 fun var_pos_eq vars x y = String.size x = String.size y andalso |
|
87 let val xs = explode x |
105 val ys = explode y |
88 val ys = explode y |
|
89 val xsys = ListPair.zip (xs,ys) |
|
90 val are_var_pairs = map (var_equiv vars) xsys |
106 in |
91 in |
107 if not_equal (length xs) (length ys) |
92 all_true are_var_pairs |
108 then |
|
109 false |
|
110 else |
|
111 let val xsys = zip xs ys |
|
112 val are_var_pairs = map (var_equiv vars) xsys |
|
113 in |
|
114 all_true are_var_pairs |
|
115 end |
|
116 end |
93 end |
117 |
|
118 |
|
119 |
94 |
120 |
95 |
121 fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list |
96 fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list |
122 |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = |
97 |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = |
123 let val y = explode x |
98 let val y = explode x |