| 1 | import re |
|---|
| 2 | import sys |
|---|
| 3 | def iscomment(line): |
|---|
| 4 | return re.match("^c",line) |
|---|
| 5 | |
|---|
| 6 | def isheader(line): |
|---|
| 7 | return re.match("^p",line) |
|---|
| 8 | |
|---|
| 9 | |
|---|
| 10 | def 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 | |
|---|
| 36 | def 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 |
|---|
| 48 | def 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 | |
|---|
| 58 | def 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"]) |
|---|
| 65 | if __name__=='__main__': |
|---|
| 66 | clauses=gen_clauses(process_input(sys.stdin)) |
|---|
| 67 | # print clauses |
|---|
| 68 | print gen_Singular(clauses) |
|---|
