source: git/Singular/cnf2ideal.py @ 28d253

spielwiese
Last change on this file since 28d253 was 28d253, checked in by Michael Brickenstein <bricken@…>, 19 years ago
*bricken: initial version of converter for DIMACS format git-svn-id: file:///usr/local/Singular/svn/trunk@8048 2c84dea3-7e68-4137-9b89-c4e89433aadc
  • Property mode set to 100644
File size: 1.9 KB
RevLine 
[28d253]1import re
2import sys
3def iscomment(line):
4    return re.match("^c",line)
5
6def isheader(line):
7    return re.match("^p",line)
8
9
10def process_input(source):
11    global vars
12    global clauses
13    input_numbers=[]
14    for line in source:
15        if (not(iscomment(line) or isheader(line))):
16            if (re.match("^%",line)):
17                break
18            line=re.sub("\n","", line)
19            line=re.sub("^\s+","",line)
20
21            ind=[int(s) for s in line.split()]
22
23            input_numbers+=ind
24           
25        else:
26            if(isheader(line)):
27                m=re.match("^p cnf\s+(?P<vars>\d+)\s+(?P<clauses>\d+)\s*\n",line)
28                assert(m)
29                #print "vars=", m.group("vars")
30                #print "clauses=",m.group("clauses")
31                vars=int(m.group("vars"))
32                clauses=int(m.group("clauses"))
33    return input_numbers
34
35
36def gen_clauses(input_numbers):
37    i=0
38    erg=[]
39    act=[]
40    for i in input_numbers:
41        if (i==0):
42            if act:
43                erg.append(act)
44                act=[]
45        else:
46            act.append(i)
47    return erg
48def gen_poly_Singular(clause):
49    def num2factor(f):
50        assert(f!=0)
51        if (f>0):
52            return "".join(["x(",str(f),")"])
53        else:
54            return "".join(["(1-x(",str(-f),"))"])
55    if clause:
56        return("*".join( [num2factor(f) for f in clause]))
57
58def gen_Singular(clauses):
59    ring_def="".join(["ring r=2,x(1..",str(vars),"),dp;"])
60    polys=[gen_poly_Singular(c) for c in clauses]
61    polys.extend(["".join(["x(",str(i),")*(x(",str(i)+")-1)"]) for i in xrange(1,vars+1)])
62    ideal="".join(["ideal i=",",\n".join(polys),";"])
63    command="std(i);"
64    return "\n".join([ring_def,ideal,command,"$;\n"])
65if __name__=='__main__':       
66    clauses=gen_clauses(process_input(sys.stdin))
67#    print clauses
68    print gen_Singular(clauses)
Note: See TracBrowser for help on using the repository browser.