source: git/Singular/cnf2ideal.py @ 79c813

spielwiese
Last change on this file since 79c813 was 79c813, checked in by Michael Brickenstein <bricken@…>, 18 years ago
*bricken: +PolyBoRi git-svn-id: file:///usr/local/Singular/svn/trunk@9342 2c84dea3-7e68-4137-9b89-c4e89433aadc
  • Property mode set to 100644
File size: 3.6 KB
Line 
1import re
2import sys
3from probstat import Cartesian
4from optparse import OptionParser
5from itertools import repeat
6from string import Template
7parser = OptionParser()
8PB="PB"
9SING="SING"
10parser.add_option("-f", "--format",
11                  action="store", dest="format", type="string", default=PB,
12                  help="select format from SING/PB")
13parser.add_option("-i", "--invert",
14                  action="store_true", dest="invert", default=False,
15                  help="invert mapping to true/false")
16
17def iscomment(line):
18    return re.match("^c",line)
19
20def isheader(line):
21    return re.match("^p",line)
22
23
24def process_input(source):
25    global vars
26    global clauses
27    input_numbers=[]
28    for line in source:
29        if (not(iscomment(line) or isheader(line))):
30            if (re.match("^%",line)):
31                break
32            line=re.sub("\n","", line)
33            line=re.sub("^\s+","",line)
34
35            ind=[int(s) for s in line.split()]
36
37            input_numbers+=ind
38           
39        else:
40            if(isheader(line)):
41                m=re.match("^p cnf\s+(?P<vars>\d+)\s+(?P<clauses>\d+)\s*\n",line)
42                assert(m)
43                #print "vars=", m.group("vars")
44                #print "clauses=",m.group("clauses")
45                vars=int(m.group("vars"))
46                clauses=int(m.group("clauses"))
47    return input_numbers
48
49
50def gen_clauses(input_numbers):
51    i=0
52    erg=[]
53    act=[]
54    for i in input_numbers:
55        if (i==0):
56            if act:
57                erg.append(act)
58                act=[]
59        else:
60            act.append(i)
61    return erg
62   
63def xor(a,b):
64    return (a and not b) or (b and not a)
65def gen_poly_Singular(clause):
66    def num2factor(f):
67        assert(f!=0)
68        if (f>0):
69            return "".join(["x(",str(f),")"])
70        else:
71            return "".join(["(1-x(",str(-f),"))"])
72    if clause:
73        return("*".join( [num2factor(f) for f in clause]))
74
75def gen_Singular(clauses):
76    ring_def="".join(["ring r=2,x(1..",str(vars),"),dp;"])
77    polys=[gen_poly_Singular(c) for c in clauses]
78    polys.extend(["".join(["x(",str(i),")*(x(",str(i)+")-1)"]) for i in xrange(1,vars+1)])
79    ideal="".join(["ideal i=",",\n".join(polys),";"])
80    command='LIB "digimult.lib";\n option(prot);\n satisfiable(i);'
81    return "\n".join([ring_def,ideal,command,"$;\n"])
82   
83def gen_poly_PB(clause):
84    def term2string(t):
85        if len(t)==0:
86            return "1"
87        return "*".join(["x("+str(v) +")" for v in t])
88   
89    vars=tuple([v for v in clause if v>0])
90    negated_vars=tuple([-v for v in clause if v<0])
91    if len(negated_vars)>0:
92        terms=[tuple([negated_vars[i] for (i,j) in enumerate(combination) if j==1])\
93            + vars for combination\
94            in Cartesian(list(repeat([0,1],len(negated_vars))))]
95    else:
96        terms=[vars]
97    res="+".join([term2string(t) for t in terms])
98    return res
99    #add_vars=[negated_var[i] for (i,j) in enumerate(combination) if j==1]
100   
101def gen_PB(clauses):
102    start_str=Template("""from PyPolyBoRi import *
103r=Ring($vars)
104def x(i):
105    return Monomial(Variable(i))
106ideal=\
107[
108""")
109    start_str=start_str.substitute(vars=vars)
110   
111   
112
113    poly_str=",\\\n   ".join([gen_poly_PB(c) for c in clauses])
114    end_str="""]
115ideal=[Polynomial(p) for p in ideal]
116"""
117    return start_str+poly_str+end_str
118   
119if __name__=='__main__':
120    (options, args) = parser.parse_args()
121    clauses=gen_clauses(process_input(sys.stdin))
122    if options.invert:
123        clauses=[[-i for i in c] for c in clauses]
124    #
125#    print clauses
126    #print gen_Singular(clauses)
127    print gen_PB(clauses)
128   
Note: See TracBrowser for help on using the repository browser.