OKlibrary  0.2.1.6
Substitutions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.7.2007 (Swansea) */
00002 /* Copyright 2008, 2009, 2013 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00024 
00025 
00026 /* ********************************************
00027    * Substitutions for variables and literals *
00028    ********************************************
00029 */
00030 
00031 /* Replace literal x via hash table h (by another literal),
00032    where h maps var_l(x) to some literal; if var_l(x) is
00033    not in the domain of the hash-map, then false resp. -false
00034    is returned. */
00035 substitute_l(x,h) := if x > 0 then ev_hm(h,x) else -ev_hm(h,-x)$
00036 
00037 
00038 /* *****************************
00039    * Substitutions for clauses *
00040    *****************************
00041 */
00042 
00043 /* Substitute literals in clause C via hash table h;
00044    possibly a pseudo-clause with clashing literals is created. */
00045 substitute_c(C,h) :=
00046  map(
00047   lambda([x],block([y:substitute_l(x,h)],
00048     if elementp(y,{false,-false}) then x else y)),
00049   C)$
00050 /* Here it is required that h covers all variables in C: */
00051 substitutetotal_c(C,h) :=
00052  map(lambda([x],substitute_l(x,h)), C)$
00053 
00054 
00055 /* *********************************
00056    * Substitutions for clause-sets *
00057    *********************************
00058 */
00059 
00060 /* Substitute literals in clause-set F via hash table h (possibly
00061    creating pseudo-clauses with clashing literals). */
00062 substitute_cs(F,h) := map(lambda([C],substitute_c(C,h)), F)$
00063 substitutetotal_cs(F,h) := map(lambda([C],substitutetotal_c(C,h)), F)$
00064 substitute_cl(F,h) := map(lambda([C],substitute_c(C,h)), F)$
00065 substitutetotal_cl(F,h) := map(lambda([C],substitutetotal_c(C,h)), F)$
00066 
00067 /* Given a list of literals of the same size as the set
00068    of variables of a formal clause-set, rename the formal
00069    clause-set, using the natural correspondence given by
00070    the given order on the set of variables.
00071 */
00072 rename_fcs(FF,L) := block(
00073  [V : listify(FF[1]), h],
00074   h : osm2hm(map("[",V,L)),
00075   [setify(abs(L)), substitutetotal_cs(FF[2],h)])$
00076 rename_cs(F,L) := fcs2cs(rename_fcs(cs2fcs(F),L))$
00077 rename_fcl(FF,L) := block(
00078  [V : FF[1], h],
00079   h : osm2hm(map("[",V,L)),
00080   [abs(L), substitutetotal_cl(FF[2],h)])$
00081 rename_cl(F,L) := fcl2cl(rename_fcl(cl2fcl(F),L))$
00082 
00083 /* The set of all renamings without flipping signs or introducing new
00084    variables of a formal clause-set FF:
00085 */
00086 all_var_renamings_fcs(FF) :=
00087  map(lambda([L], rename_fcs(FF,L)), permutations(FF[1]))$
00088 /* The set of all sign-flippings of a formal clause-set FF: */
00089 all_sign_flippings_fcs(FF) := block([V : listify(FF[1])],
00090  map(lambda([L], rename_fcs(FF,L*V)), all_tuples({-1,1},length(V))))$
00091 /* The set of all renamings without introducing new variables
00092    of a formal clause-set FF:
00093 */
00094 all_renamings_fcs(FF) := lunion(map(all_sign_flippings_fcs, all_var_renamings_fcs(FF)))$
00095 
00096 
00097 /* Translating variable names of a formal clause-set into natural numbers;
00098    outputs a pair consisting of the translated formal clause-set and
00099    the list of old variable names (positions corresponding to new
00100    variable-numbers) */
00101 standardise_fcs(FF) := block([L : create_list(i,i,1,nvar_f(FF))],
00102  [rename_fcs(FF,L), listify(var_cs_f(FF))])$
00103 standardise_fcl(FF) := block([L : create_list(i,i,1,length(FF[1]))],
00104  [rename_fcl(FF,L), FF[1]])$
00105 
00106 
00107 /* Make a list of formal clause-sets variable-disjoint, using
00108    variables from 1 on. Returns a pair consisting of the renamed
00109    list and the total number n of variables (so the next free
00110    variable is n+1). */
00111 make_vardisjoint_fcs(LFF) := block([index : 0, result : []],
00112   for FF in LFF do block([n : nvar_f(FF)],
00113     result : endcons(rename_fcs(FF,create_list(index + i, i,1,n)), result),
00114     index : index + n),
00115   return([result, index]))$
00116 /* Returning now a triple, with the list of lists of old variables as third
00117    component (corresponding to the new variable-numbers):
00118 */
00119 make_vardisjoint_vl_fcs(LFF) :=
00120  endcons(map(listify,map(first,LFF)), make_vardisjoint_fcs(LFF))$
00121