1 | import re |
---|
2 | import sys |
---|
3 | from probstat import Cartesian |
---|
4 | from optparse import OptionParser |
---|
5 | from itertools import repeat |
---|
6 | from string import Template |
---|
7 | from re import sub |
---|
8 | parser = OptionParser() |
---|
9 | PB="PB" |
---|
10 | SING="SING" |
---|
11 | ALL="all" |
---|
12 | parser.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") |
---|
18 | parser.add_option("-i", "--invert", |
---|
19 | action="store_true", dest="invert", default=False, |
---|
20 | help="invert mapping to true/false") |
---|
21 | |
---|
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 |
---|
67 | |
---|
68 | def xor(a,b): |
---|
69 | return (a and not b) or (b and not a) |
---|
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): |
---|
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 | |
---|
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]) |
---|
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 | |
---|
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] |
---|
146 | try: |
---|
147 | del p |
---|
148 | except: |
---|
149 | pass |
---|
150 | |
---|
151 | """ |
---|
152 | return start_str+poly_str+end_str |
---|
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() |
---|
185 | |
---|
186 | |
---|
187 | def 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 | |
---|
204 | if __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) |
---|