source: git/Singular/cnf2ideal.py @ 1b2216

spielwiese
Last change on this file since 1b2216 was 0e9ea9, checked in by Michael Brickenstein <bricken@…>, 18 years ago
+ cleanup git-svn-id: file:///usr/local/Singular/svn/trunk@9358 2c84dea3-7e68-4137-9b89-c4e89433aadc
  • Property mode set to 100644
File size: 6.4 KB
Line 
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)
Note: See TracBrowser for help on using the repository browser.