load("HashMaps.lisp")\$ var_l(x) := abs(x)\$ var_sl(C) := map(var_l, C)\$ var_c(C) := map(var_l, C)\$ var_cs(F) := var_sl(apply(union,listify(F)))\$ var_cs_f(FF) := FF[1]\$ fcs2cs(FF) := second(FF)\$ substitute_l(x,h) := if x > 0 then ev_hm(h,x) else -ev_hm(h,-x)\$ substitute_c(C,h) := map( lambda([x],block([y:substitute_l(x,h)], if elementp(y,{false,-false}) then x else y)), C)\$ substitutetotal_c(C,h) := map(lambda([x],substitute_l(x,h)), C)\$ substitutetotal_cs(F,h) := map(lambda([C],substitutetotal_c(C,h)), F)\$ rename_fcs(FF,L) := block( [V : listify(FF[1]), h], h : osm2hm(map("[",V,L)), [setify(abs(L)), substitutetotal_cs(FF[2],h)])\$ standardise_fcs(FF) := block([L : create_list(i,i,1,nvar_f(FF))], [rename_fcs(FF,L), listify(var_cs_f(FF))])\$ variable_degrees_cs(F) := block([h : sm2hm({})], for C in F do for v in var_c(C) do enter_new_occurrence(h,v), return(h))\$ min_variable_degree_cs(F) := lmin(map(lambda([A],part(A,2)),hm2sm(variable_degrees_cs(F))))\$ corr_cartesian_product([S]) := if emptyp(S) then {[]} else apply(cartesian_product,S)\$ all_tass(V) := map(setify,apply(corr_cartesian_product, map(lambda([v],{-v,v}),listify(V))))\$ setn(n) := setify(create_list(i,i,1,n))\$ full_fcs_v(V) := [V,all_tass(V)]\$ full_fcs(n) := full_fcs_v(setn(n))\$ set_hm(h,x,y) := set_hash_okl(sconcat(x),h,y)\$ ev_hm(h,x) := get_hash_okl(sconcat(x),h)\$ ev_hm_d(h,x,y) := get_hash_okl(sconcat(x),h,y)\$ del_hm(h,x) := del_hash_okl(sconcat(x),h)\$ sm2hm(M) := block([h : hash_table_okl()], for p in M do set_hm(h,p[1],p[2]), return(h))\$ osm2hm(M) := sm2hm(M)\$ hm2osm(h) := map(lambda([a],[eval_string(part(a,1)),part(a,2)]),hash_table_data_okl(h))\$ hm2sm(h) := setify(hm2osm(h))\$ enter_new_occurrence(h,x) := set_hm(h,x,ev_hm_d(h,x,0)+1)\$ get_distribution(h) := listify(hm2sm(h))\$ h : sm2hm({}); nvar_f(FF) := length(FF[1])\$ ncl_f(FF) := length(clauses_f(FF))\$ clauses_f(FF) := FF[2]\$ literals_v(V) := block([L : listify(V)], setify(append(L,-L)))\$ literal_degrees_cs(F) := block([h : sm2hm({})], for C in F do for x in C do enter_new_occurrence(h,x), return(h))\$ all_literal_degrees_fcs(FF) := block( [h : literal_degrees_cs(FF[2]), L : literals_v(FF[1])], for x in L do if ev_hm(h,x) = false then set_hm(h,x,0), return(h))\$ literal_degrees_list_fcs(FF) := block( [litdeg : hm2sm(all_literal_degrees_fcs(FF)), h : sm2hm({})], for p in litdeg do enter_new_occurrence(h,p[2]), get_distribution(h))\$ ncl_list_f(FF) := block( [n : nvar_f(FF), counts, res : []], counts : make_array(fixnum, n+1), for C in FF[2] do block([l : length(C)], counts[l] : counts[l] + 1), for i : 0 thru n do if counts[i] # 0 then res : endcons([i, counts[i]], res), return(res))\$ fcs_identifier(FF) := [nvar_f(FF), ncl_f(FF), literal_degrees_list_fcs(FF), ncl_list_f(FF)]\$ is_isomorphic_btr_fcs(FF1,FF2) := block( if elementp({},FF1[2]) then ( if not elementp({},FF2[2]) then return(false)) elseif elementp({},FF2[2]) then return(false), block( [V1o : var_cs(FF1[2]), V2o : var_cs(FF2[2]), F1r, F2r, n, V, F1, F2, degl1, degl2, map_poss : []], if nvar_f(FF1) # nvar_f(FF2) then return(false), if length(V1o) # length(V2o) then return(false), n : length(V1o), V : setn(n), if emptyp(V) then return(true), F1r : standardise_fcs([V1o,FF1[2]]), F2r : standardise_fcs([V2o,FF2[2]]), F1 : disjoin({},F1r[1][2]), F2 : disjoin({},F2r[1][2]), degl1 : all_literal_degrees_fcs([V,F1]), degl2 : all_literal_degrees_fcs([V,F2]), block([deg_pairs : sm2hm({})], for v in V do block([deg : [ev_hm(degl2,v), ev_hm(degl2,-v)]], if deg[1] = deg[2] then set_hm(deg_pairs, deg, union({v,-v}, ev_hm_d(deg_pairs, deg, {}))) else ( set_hm(deg_pairs, deg, adjoin(v, ev_hm_d(deg_pairs, deg, {}))), set_hm(deg_pairs, reverse(deg), adjoin(-v, ev_hm_d(deg_pairs, reverse(deg), {})))) ), for v in V do block([deg : [ev_hm(degl1,v), ev_hm(degl1,-v)]], map_poss : endcons([v,ev_hm_d(deg_pairs, deg, {})], map_poss)) ), map_poss : sort(map_poss, lambda([p1,p2], is(length(p1[2]) < length(p2[2])))), is_isomorphic_btr_piso(sm2hm({}), {}, map_poss, F1)))\$ is_isomorphic_btr_piso(part_iso,domain_piso,map_possibilities,rem_clauses) := block( [B : first(map_possibilities), v, Y, found_iso : false], v : B[1], Y : B[2], domain_piso : adjoin(v,domain_piso), for y in Y unless found_iso do block( [inconsistent : false, to_be_removed : {}], set_hm(part_iso,v,y), for C in rem_clauses unless inconsistent do ( if subsetp(var_c(C), domain_piso) then if not elementp(substitute_c(C,part_iso), F2) then inconsistent : true else to_be_removed : adjoin(C,to_be_removed) ), if not inconsistent then block( [new_rem_clauses : setdifference(rem_clauses, to_be_removed), new_map_possibilities : copylist(rest(map_possibilities))], if emptyp(new_rem_clauses) then found_iso : true else ( for i : 1 thru length(new_map_possibilities) do block( [P : new_map_possibilities[i]], new_map_possibilities[i] : [P[1], setdifference(P[2],{y,-y})]), new_map_possibilities : sort(new_map_possibilities, lambda([p1,p2], is(length(p1[2]) < length(p2[2])))), if is_isomorphic_btr_piso( part_iso,domain_piso,new_map_possibilities,new_rem_clauses) then found_iso : true ) ) ), del_hm(part_iso,v), return(found_iso))\$ manage_repository_isomorphism_types(FF, repo) := block( [p : fcs_identifier(FF), candidates], candidates : ev_hm(repo,p), if candidates = false then ( set_hm(repo,p,{FF}), return(true)) else block([found : false], for GG in candidates unless found do if is_isomorphic_btr_fcs(FF,GG) then found : true, if found then return(false) else ( set_hm(repo,p,adjoin(FF,candidates)), return(true))))\$ manage_repository_isomorphism_types(full_fcs(8), h)\$ max_min_var_degree_def_rec[k] := if k = 1 then 2 else lmax(create_list(min(2*i,max_min_var_degree_def_rec[k-i+1]+i),i,2,k))\$ analyse_isorepo_defset_mvd(repository) := block( [M : hm2sm(repository), h : sm2hm({})], for P in M do block([def : P[1][2] - P[1][1], mvd], mvd : max_min_var_degree_def_rec[def], set_hm(h,def,union(ev_hm_d(h,def,{}), subset(map(fcs2cs,P[2]), lambda([F],is(min_variable_degree_cs(F)=mvd ))))) ), sort(listify(hm2sm(h)),lambda([P1,P2], is(P1[1] < P2[1]))))\$ analyse_isorepo_defset_mvd(h);