1.1 --- a/src/HOL/Tools/res_clause.ML Fri Dec 16 11:51:24 2005 +0100
1.2 +++ b/src/HOL/Tools/res_clause.ML Fri Dec 16 12:15:54 2005 +0100
1.3 @@ -69,9 +69,13 @@
1.4 val gen_tptp_type_cls : int * string * string * string * int -> string
1.5 val tptp_of_typeLit : type_literal -> string
1.6
1.7 + (*for hashing*)
1.8 + val clause_eq : clause * clause -> bool
1.9 + val hash1_clause : clause -> word
1.10 +
1.11 end;
1.12
1.13 -structure ResClause: RES_CLAUSE =
1.14 +structure ResClause : RES_CLAUSE =
1.15 struct
1.16
1.17 (* Added for typed equality *)
1.18 @@ -412,7 +416,6 @@
1.19 (union_all (ts1::ts2),
1.20 union_all(funcs::funcs')))
1.21 end
1.22 - | term_of t = raise CLAUSE("Function Not First Order 4", t)
1.23 and terms_of ts =
1.24 let val (args, ts_funcs) = ListPair.unzip (map term_of ts)
1.25 in
1.26 @@ -505,21 +508,16 @@
1.27 | term_ord (UVar(_,_),_) = LESS
1.28 | term_ord (Fun(_,_,_),UVar(_)) = GREATER
1.29 | term_ord (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) =
1.30 - let val fn_ord = string_ord (f1,f2)
1.31 - in
1.32 - case fn_ord of EQUAL =>
1.33 - let val tms_ord = terms_ord (tms1,tms2)
1.34 - in
1.35 - case tms_ord of EQUAL => types_ord (tps1,tps2)
1.36 - | _ => tms_ord
1.37 - end
1.38 - | _ => fn_ord
1.39 - end
1.40 + (case string_ord (f1,f2) of
1.41 + EQUAL =>
1.42 + (case terms_ord (tms1,tms2) of EQUAL => types_ord (tps1,tps2)
1.43 + | tms_ord => tms_ord)
1.44 + | fn_ord => fn_ord)
1.45
1.46 and
1.47
1.48 -terms_ord ([],[]) = EQUAL
1.49 - | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2);
1.50 + terms_ord ([],[]) = EQUAL
1.51 + | terms_ord (tms1,tms2) = list_ord term_ord (tms1,tms2);
1.52
1.53
1.54
1.55 @@ -541,6 +539,7 @@
1.56
1.57 fun sort_lits lits = sort literal_ord lits;
1.58
1.59 +
1.60 (********** clause equivalence ******************)
1.61
1.62 fun check_var_pairs (x,y) [] = 0
1.63 @@ -550,7 +549,6 @@
1.64 if (x = u) orelse (y = v) then 2 (*conflict*)
1.65 else check_var_pairs (x,y) w;
1.66
1.67 -
1.68 fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) =
1.69 (case check_var_pairs (v1,v2) tvars of 0 => (true,(vars,(v1,v2)::tvars))
1.70 | 1 => (true,(vars,tvars))
1.71 @@ -559,24 +557,24 @@
1.72 | type_eq (AtomF(f1),AtomF(f2)) vtvars = (f1=f2,vtvars)
1.73 | type_eq (AtomF(_),_) vtvars = (false,vtvars)
1.74 | type_eq (Comp(con1,args1),Comp(con2,args2)) vtvars =
1.75 - let val (eq1,vtvars1) =
1.76 - if (con1 = con2) then types_eq (args1,args2) vtvars
1.77 - else (false,vtvars)
1.78 - in
1.79 - (eq1,vtvars1)
1.80 - end
1.81 + let val (eq1,vtvars1) =
1.82 + if con1 = con2 then types_eq (args1,args2) vtvars
1.83 + else (false,vtvars)
1.84 + in
1.85 + (eq1,vtvars1)
1.86 + end
1.87 | type_eq (Comp(_,_),_) vtvars = (false,vtvars)
1.88
1.89 and
1.90
1.91 -types_eq ([],[]) vtvars = (true,vtvars)
1.92 -| types_eq (tp1::tps1,tp2::tps2) vtvars =
1.93 - let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars
1.94 - val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1
1.95 - else (eq1,vtvars1)
1.96 - in
1.97 - (eq2,vtvars2)
1.98 - end;
1.99 + types_eq ([],[]) vtvars = (true,vtvars)
1.100 + | types_eq (tp1::tps1,tp2::tps2) vtvars =
1.101 + let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars
1.102 + val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1
1.103 + else (eq1,vtvars1)
1.104 + in
1.105 + (eq2,vtvars2)
1.106 + end;
1.107
1.108
1.109 fun term_eq (UVar(v1,tp1),UVar(v2,tp2)) (vars,tvars) =
1.110 @@ -585,27 +583,27 @@
1.111 | 2 => (false,(vars,tvars)))
1.112 | term_eq (UVar(_,_),_) vtvars = (false,vtvars)
1.113 | term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars =
1.114 - let val (eq1,vtvars1) =
1.115 - if (f1 = f2) then terms_eq (tms1,tms2) vtvars
1.116 - else (false,vtvars)
1.117 - val (eq2,vtvars2) =
1.118 - if eq1 then types_eq (tps1,tps2) vtvars1
1.119 - else (eq1,vtvars1)
1.120 - in
1.121 - (eq2,vtvars2)
1.122 - end
1.123 + let val (eq1,vtvars1) =
1.124 + if f1 = f2 then terms_eq (tms1,tms2) vtvars
1.125 + else (false,vtvars)
1.126 + val (eq2,vtvars2) =
1.127 + if eq1 then types_eq (tps1,tps2) vtvars1
1.128 + else (eq1,vtvars1)
1.129 + in
1.130 + (eq2,vtvars2)
1.131 + end
1.132 | term_eq (Fun(_,_,_),_) vtvars = (false,vtvars)
1.133
1.134 and
1.135
1.136 -terms_eq ([],[]) vtvars = (true,vtvars)
1.137 -| terms_eq (tm1::tms1,tm2::tms2) vtvars =
1.138 - let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars
1.139 - val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1
1.140 - else (eq1,vtvars1)
1.141 - in
1.142 - (eq2,vtvars2)
1.143 - end;
1.144 + terms_eq ([],[]) vtvars = (true,vtvars)
1.145 + | terms_eq (tm1::tms1,tm2::tms2) vtvars =
1.146 + let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars
1.147 + val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1
1.148 + else (eq1,vtvars1)
1.149 + in
1.150 + (eq2,vtvars2)
1.151 + end;
1.152
1.153
1.154 fun pred_eq (Predicate(predname1,tps1,tms1),Predicate(predname2,tps2,tms2)) vtvars =
1.155 @@ -634,14 +632,30 @@
1.156 end;
1.157
1.158
1.159 -fun cls_eq (cls1,cls2) =
1.160 +(*Equality of two clauses up to variable renaming*)
1.161 +fun clause_eq (cls1,cls2) =
1.162 let val lits1 = get_literals cls1
1.163 val lits2 = get_literals cls2
1.164 in
1.165 - (length lits1 = length lits2) andalso (fst (lits_eq (lits1,lits2) ([],[])))
1.166 + length lits1 = length lits2 andalso #1 (lits_eq (lits1,lits2) ([],[]))
1.167 end;
1.168
1.169
1.170 +(*** Hash function for clauses ***)
1.171 +
1.172 +val xor_words = List.foldl Word.xorb 0w0;
1.173 +
1.174 +fun hash_term (UVar(_,_), w) = w
1.175 + | hash_term (Fun(f,tps,args), w) =
1.176 + List.foldl hash_term (Hashtable.hash_string (f,w)) args;
1.177 +
1.178 +fun hash_pred (Predicate(pn,_,args), w) =
1.179 + List.foldl hash_term (Hashtable.hash_string (pn,w)) args;
1.180 +
1.181 +fun hash1_literal (Literal(true,pred,_)) = hash_pred (pred, 0w0)
1.182 + | hash1_literal (Literal(false,pred,_)) = Word.notb (hash_pred (pred, 0w0));
1.183 +
1.184 +fun hash1_clause clause = xor_words (map hash1_literal (get_literals clause));
1.185
1.186
1.187 (* FIX: not sure what to do with these funcs *)
1.188 @@ -808,7 +822,8 @@
1.189 premLits = map make_TVarLit false_tvars_srts'}
1.190 end;
1.191
1.192 -(*The number of clauses generated from cls, including type clauses*)
1.193 +(*The number of clauses generated from cls, including type clauses. It's always 1
1.194 + except for conjecture clauses.*)
1.195 fun num_of_clauses (Clause cls) =
1.196 let val num_tfree_lits =
1.197 if !keep_types then length (#tfree_type_literals cls)
1.198 @@ -886,17 +901,14 @@
1.199 | string_of_term (Fun (name,typs,terms)) =
1.200 let val terms_as_strings = map string_of_term terms
1.201 val typs' = if !keep_types then map string_of_fol_type typs else []
1.202 - in name ^ (paren_pack (terms_as_strings @ typs')) end
1.203 - | string_of_term _ = error "string_of_term";
1.204 + in name ^ (paren_pack (terms_as_strings @ typs')) end;
1.205
1.206 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
1.207 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
1.208 | string_of_predicate (Predicate(name,typs,terms)) =
1.209 let val terms_as_strings = map string_of_term terms
1.210 val typs' = if !keep_types then map string_of_fol_type typs else []
1.211 - in name ^ (paren_pack (terms_as_strings @ typs')) end
1.212 - | string_of_predicate _ = error "string_of_predicate";
1.213 -
1.214 + in name ^ (paren_pack (terms_as_strings @ typs')) end;
1.215
1.216 fun string_of_clausename (cls_id,ax_name) =
1.217 clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;