[28d253] | 1 | import re |
---|
| 2 | import sys |
---|
[79c813] | 3 | from probstat import Cartesian |
---|
| 4 | from optparse import OptionParser |
---|
| 5 | from itertools import repeat |
---|
| 6 | from string import Template |
---|
[d420d9] | 7 | from re import sub |
---|
[79c813] | 8 | parser = OptionParser() |
---|
| 9 | PB="PB" |
---|
| 10 | SING="SING" |
---|
[d420d9] | 11 | ALL="all" |
---|
[79c813] | 12 | parser.add_option("-f", "--format", |
---|
[d420d9] | 13 | action="store", dest="format", type="string", default=ALL, |
---|
[79c813] | 14 | help="select format from SING/PB") |
---|
[d420d9] | 15 | #parser.add_option("-c", "--cnf", |
---|
| 16 | # action="store", dest="cnf", type="string", default=None, |
---|
| 17 | # help="select input cnf") |
---|
[79c813] | 18 | parser.add_option("-i", "--invert", |
---|
| 19 | action="store_true", dest="invert", default=False, |
---|
| 20 | help="invert mapping to true/false") |
---|
| 21 | |
---|
[28d253] | 22 | def iscomment(line): |
---|
| 23 | return re.match("^c",line) |
---|
| 24 | |
---|
| 25 | def isheader(line): |
---|
| 26 | return re.match("^p",line) |
---|
| 27 | |
---|
| 28 | |
---|
| 29 | def process_input(source): |
---|
| 30 | global vars |
---|
| 31 | global clauses |
---|
| 32 | input_numbers=[] |
---|
| 33 | for line in source: |
---|
| 34 | if (not(iscomment(line) or isheader(line))): |
---|
| 35 | if (re.match("^%",line)): |
---|
| 36 | break |
---|
| 37 | line=re.sub("\n","", line) |
---|
| 38 | line=re.sub("^\s+","",line) |
---|
| 39 | |
---|
| 40 | ind=[int(s) for s in line.split()] |
---|
| 41 | |
---|
| 42 | input_numbers+=ind |
---|
| 43 | |
---|
| 44 | else: |
---|
| 45 | if(isheader(line)): |
---|
| 46 | m=re.match("^p cnf\s+(?P<vars>\d+)\s+(?P<clauses>\d+)\s*\n",line) |
---|
| 47 | assert(m) |
---|
| 48 | #print "vars=", m.group("vars") |
---|
| 49 | #print "clauses=",m.group("clauses") |
---|
| 50 | vars=int(m.group("vars")) |
---|
| 51 | clauses=int(m.group("clauses")) |
---|
| 52 | return input_numbers |
---|
| 53 | |
---|
| 54 | |
---|
| 55 | def gen_clauses(input_numbers): |
---|
| 56 | i=0 |
---|
| 57 | erg=[] |
---|
| 58 | act=[] |
---|
| 59 | for i in input_numbers: |
---|
| 60 | if (i==0): |
---|
| 61 | if act: |
---|
| 62 | erg.append(act) |
---|
| 63 | act=[] |
---|
| 64 | else: |
---|
| 65 | act.append(i) |
---|
| 66 | return erg |
---|
[79c813] | 67 | |
---|
| 68 | def xor(a,b): |
---|
| 69 | return (a and not b) or (b and not a) |
---|
[28d253] | 70 | def gen_poly_Singular(clause): |
---|
| 71 | def num2factor(f): |
---|
| 72 | assert(f!=0) |
---|
| 73 | if (f>0): |
---|
| 74 | return "".join(["x(",str(f),")"]) |
---|
| 75 | else: |
---|
| 76 | return "".join(["(1-x(",str(-f),"))"]) |
---|
| 77 | if clause: |
---|
| 78 | return("*".join( [num2factor(f) for f in clause])) |
---|
| 79 | |
---|
| 80 | def gen_Singular(clauses): |
---|
[d420d9] | 81 | ring_def="".join(["ring r=2,x(1..",str(vars),"),lp;"]) |
---|
[28d253] | 82 | polys=[gen_poly_Singular(c) for c in clauses] |
---|
| 83 | polys.extend(["".join(["x(",str(i),")*(x(",str(i)+")-1)"]) for i in xrange(1,vars+1)]) |
---|
| 84 | ideal="".join(["ideal i=",",\n".join(polys),";"]) |
---|
[d420d9] | 85 | #command='LIB "digimult.lib";\n option(prot);\n satisfiable(i);' |
---|
| 86 | command='option(redTail);\noption(prot);\nstd(i);\n' |
---|
[28d253] | 87 | return "\n".join([ring_def,ideal,command,"$;\n"]) |
---|
[d8e1214] | 88 | |
---|
| 89 | |
---|
| 90 | def gen_poly_Magma(clause): |
---|
| 91 | def num2factor(f): |
---|
| 92 | assert(f!=0) |
---|
| 93 | if (f>0): |
---|
| 94 | return "".join(["x",str(f),""]) |
---|
| 95 | else: |
---|
| 96 | return "".join(["(1-x",str(-f),")"]) |
---|
| 97 | if clause: |
---|
| 98 | return("*".join( [num2factor(f) for f in clause])) |
---|
| 99 | |
---|
| 100 | def gen_Magma(clauses): |
---|
| 101 | start_str=Template("""F:=FiniteField(2); |
---|
| 102 | R< $var_list >:=PolynomialRing(F,$nvars,"lex"); |
---|
| 103 | i:=ideal< R | $ideal |
---|
| 104 | >; |
---|
| 105 | GroebnerBasis(i); |
---|
| 106 | exit; |
---|
| 107 | """) |
---|
| 108 | var_list=", ".join(["x"+str(i+1) for i in xrange(vars)]) |
---|
| 109 | ideal=",\n".join([gen_poly_Magma(p) for p in clauses]) |
---|
[d961eb] | 110 | ideal=ideal+",\n"+",\n".join(["x"+str(i)+"^2+x"+str(i) for i in xrange(1,vars+1)]) |
---|
[d8e1214] | 111 | return start_str.substitute({"nvars":str(vars), "var_list":var_list, "ideal":ideal}) |
---|
[79c813] | 112 | |
---|
| 113 | def gen_poly_PB(clause): |
---|
| 114 | def term2string(t): |
---|
| 115 | if len(t)==0: |
---|
| 116 | return "1" |
---|
| 117 | return "*".join(["x("+str(v) +")" for v in t]) |
---|
| 118 | |
---|
| 119 | vars=tuple([v for v in clause if v>0]) |
---|
| 120 | negated_vars=tuple([-v for v in clause if v<0]) |
---|
| 121 | if len(negated_vars)>0: |
---|
| 122 | terms=[tuple([negated_vars[i] for (i,j) in enumerate(combination) if j==1])\ |
---|
| 123 | + vars for combination\ |
---|
| 124 | in Cartesian(list(repeat([0,1],len(negated_vars))))] |
---|
| 125 | else: |
---|
| 126 | terms=[vars] |
---|
| 127 | res="+".join([term2string(t) for t in terms]) |
---|
| 128 | return res |
---|
| 129 | #add_vars=[negated_var[i] for (i,j) in enumerate(combination) if j==1] |
---|
| 130 | |
---|
| 131 | def gen_PB(clauses): |
---|
| 132 | start_str=Template("""from PyPolyBoRi import * |
---|
| 133 | r=Ring($vars) |
---|
| 134 | def x(i): |
---|
| 135 | return Monomial(Variable(i)) |
---|
| 136 | ideal=\ |
---|
| 137 | [ |
---|
| 138 | """) |
---|
| 139 | start_str=start_str.substitute(vars=vars) |
---|
| 140 | |
---|
| 141 | |
---|
| 142 | |
---|
| 143 | poly_str=",\\\n ".join([gen_poly_PB(c) for c in clauses]) |
---|
| 144 | end_str="""] |
---|
| 145 | ideal=[Polynomial(p) for p in ideal] |
---|
[0e9ea9] | 146 | try: |
---|
| 147 | del p |
---|
| 148 | except: |
---|
| 149 | pass |
---|
| 150 | |
---|
[79c813] | 151 | """ |
---|
| 152 | return start_str+poly_str+end_str |
---|
[d420d9] | 153 | |
---|
| 154 | from re import sub |
---|
| 155 | def convert_file_PB(cnf,invert): |
---|
| 156 | clauses=gen_clauses(process_input(open(cnf))) |
---|
| 157 | #clauses=gen_clauses(process_input(sys.stdin)) |
---|
| 158 | if invert: |
---|
| 159 | clauses=[[-i for i in c] for c in clauses] |
---|
| 160 | # |
---|
| 161 | # print clauses |
---|
| 162 | #print gen_Singular(clauses) |
---|
| 163 | out_file_name=cnf[:-3]+"py" |
---|
| 164 | if invert: |
---|
| 165 | out_file_name=out_file_name[:-3]+"Inverted.py" |
---|
| 166 | out_file_name=sub("-","_",out_file_name) |
---|
| 167 | out=open(out_file_name,"w") |
---|
| 168 | out.write(gen_PB(clauses)) |
---|
| 169 | out.close() |
---|
| 170 | def convert_file_Singular(cnf,invert): |
---|
| 171 | clauses=gen_clauses(process_input(open(cnf))) |
---|
| 172 | |
---|
| 173 | #clauses=gen_clauses(process_input(sys.stdin)) |
---|
| 174 | if invert: |
---|
| 175 | clauses=[[-i for i in c] for c in clauses] |
---|
| 176 | # |
---|
| 177 | # print clauses |
---|
| 178 | #print gen_Singular(clauses) |
---|
| 179 | out_file_name=cnf[:-3]+"sing" |
---|
| 180 | if invert: |
---|
| 181 | out_file_name=out_file_name[:-5]+"Inverted.sing" |
---|
| 182 | out=open(out_file_name,"w") |
---|
| 183 | out.write(gen_Singular(clauses)) |
---|
| 184 | out.close() |
---|
[d8e1214] | 185 | |
---|
| 186 | |
---|
| 187 | def convert_file_Magma(cnf,invert): |
---|
| 188 | clauses=gen_clauses(process_input(open(cnf))) |
---|
[d420d9] | 189 | |
---|
[d8e1214] | 190 | #clauses=gen_clauses(process_input(sys.stdin)) |
---|
| 191 | if invert: |
---|
| 192 | clauses=[[-i for i in c] for c in clauses] |
---|
| 193 | # |
---|
| 194 | # print clauses |
---|
| 195 | #print gen_Singular(clauses) |
---|
| 196 | out_file_name=cnf[:-3]+"magma" |
---|
| 197 | if invert: |
---|
| 198 | out_file_name=out_file_name[:-6]+"Inverted.magma" |
---|
| 199 | out=open(out_file_name,"w") |
---|
| 200 | #print out |
---|
| 201 | out.write(gen_Magma(clauses)) |
---|
| 202 | out.close() |
---|
[79c813] | 203 | |
---|
| 204 | if __name__=='__main__': |
---|
| 205 | (options, args) = parser.parse_args() |
---|
[d420d9] | 206 | #clauses=gen_clauses(process_input(open(options.cnf))) |
---|
| 207 | #clauses=gen_clauses(process_input(sys.stdin)) |
---|
| 208 | #if options.invert: |
---|
| 209 | # clauses=[[-i for i in c] for c in clauses] |
---|
[79c813] | 210 | # |
---|
[28d253] | 211 | # print clauses |
---|
[79c813] | 212 | #print gen_Singular(clauses) |
---|
[d420d9] | 213 | #out_file_name=options.cnf[:-3]+"py" |
---|
| 214 | #if options.invert: |
---|
| 215 | # out_file_name=out_file_name[:-3]+"Inverted.py" |
---|
| 216 | #out=open(out_file_name,"w") |
---|
| 217 | #out.write(gen_PB(clauses)) |
---|
| 218 | #out.close() |
---|
| 219 | for a in args: |
---|
| 220 | if options.format==ALL: |
---|
| 221 | convert_file_PB(a, options.invert) |
---|
| 222 | convert_file_Singular(a, options.invert) |
---|
[d8e1214] | 223 | convert_file_Magma(a, options.invert) |
---|