1import re 2import sys 3from probstat import Cartesian 4from optparse import OptionParser 5from itertools import repeat 6from string import Template 7from re import sub 8parser = OptionParser() 9PB="PB" 10SING="SING" 11ALL="all" 12parser.add_option("-f", "--format", 13 action="store", dest="format", type="string", default=ALL, 14 help="select format from SING/PB") 15#parser.add_option("-c", "--cnf", 16# action="store", dest="cnf", type="string", default=None, 17# help="select input cnf") 18parser.add_option("-i", "--invert", 19 action="store_true", dest="invert", default=False, 20 help="invert mapping to true/false") 21 22def iscomment(line): 23 return re.match("^c",line) 24 25def isheader(line): 26 return re.match("^p",line) 27 28 29def 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 55def 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 67 68def xor(a,b): 69 return (a and not b) or (b and not a) 70def 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 80def gen_Singular(clauses): 81 ring_def="".join(["ring r=2,x(1..",str(vars),"),lp;"]) 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),";"]) 85 #command='LIB "digimult.lib";\n option(prot);\n satisfiable(i);' 86 command='option(redTail);\noption(prot);\nstd(i);\n' 87 return "\n".join([ring_def,ideal,command,"$;\n"]) 88 89 90def 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 100def gen_Magma(clauses): 101 start_str=Template("""F:=FiniteField(2); 102R< $var_list >:=PolynomialRing(F,$nvars,"lex"); 103i:=ideal< R | $ideal 104>; 105GroebnerBasis(i); 106exit; 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]) 110 ideal=ideal+",\n"+",\n".join(["x"+str(i)+"^2+x"+str(i) for i in xrange(1,vars+1)]) 111 return start_str.substitute({"nvars":str(vars), "var_list":var_list, "ideal":ideal}) 112 113def 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 131def gen_PB(clauses): 132 start_str=Template("""from PyPolyBoRi import * 133r=Ring($vars) 134def x(i): 135 return Monomial(Variable(i)) 136ideal=\ 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="""] 145ideal=[Polynomial(p) for p in ideal] 146try: 147 del p 148except: 149 pass 150 151""" 152 return start_str+poly_str+end_str 153 154from re import sub 155def 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() 170def 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() 185 186 187def convert_file_Magma(cnf,invert): 188 clauses=gen_clauses(process_input(open(cnf))) 189 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() 203 204if __name__=='__main__': 205 (options, args) = parser.parse_args() 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] 210 # 211# print clauses 212 #print gen_Singular(clauses) 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) 223 convert_file_Magma(a, options.invert)