1.1 --- a/sml.py	Mon May 30 15:51:01 2011 +0200
     1.2 +++ b/sml.py	Tue May 31 00:58:51 2011 +0200
     1.3 @@ -4,6 +4,9 @@
     1.4  Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
     1.5  """
     1.6  
     1.7 +TMP_DIMACS = "dimacs~"
     1.8 +TMP_SOLUTION = "solution~"
     1.9 +
    1.10  def main():
    1.11      # edit your formulae here
    1.12      p = Variable("p")
    1.13 @@ -41,12 +44,42 @@
    1.14      print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 
    1.15      formula = mcnf(formula)
    1.16      print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
    1.17 -    cnf_formula = cnf(original)
    1.18 -    print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
    1.19 +    #cnf_formula = cnf(original)
    1.20 +    #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
    1.21 +    
    1.22 +    if not args.dimacs:
    1.23 +        dimacs_file = TMP_DIMACS
    1.24 +    else:
    1.25 +        dimacs_file = args.dimacs
    1.26 +    solution = sat_test(original, dimacs_file)
    1.27 +    if solution:
    1.28 +        print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution]))
    1.29 +    else:
    1.30 +        print "not satisfiable"
    1.31 +    
    1.32 +from subprocess import call, PIPE
    1.33  
    1.34 -    if (args.dimacs):
    1.35 -        with open(args.dimacs, "w") as f:
    1.36 -            f.write(dimacs(formula))           
    1.37 +def sat_test(formula, dimacs_file):
    1.38 +    out, variables = dimacs(formula)
    1.39 +    with open(dimacs_file, "w") as f:
    1.40 +        f.write(out) 
    1.41 +    call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE)
    1.42 +    with open(TMP_SOLUTION) as f:
    1.43 +        solved, assignment = f.readlines()  
    1.44 +    solved = solved[0] == "S"      
    1.45 +    if solved:
    1.46 +        positive = set() 
    1.47 +        for a in assignment.split():           
    1.48 +            neg = a[0] == "-"
    1.49 +            if not neg:
    1.50 +                positive.add(int(a))       
    1.51 +        solution = []
    1.52 +        for v, n in variables.iteritems():           
    1.53 +            if n in positive:              
    1.54 +                solution.append(Variable(v))
    1.55 +            else:
    1.56 +                solution.append(Not(Variable(v)))
    1.57 +        return solution
    1.58  
    1.59  def dimacs(formula):
    1.60      def clausify(f):        
    1.61 @@ -79,7 +112,7 @@
    1.62      out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
    1.63      out += "p cnf %i %i\n" % (len(variables), len(clauses))    
    1.64      out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
    1.65 -    return out
    1.66 +    return out, variables
    1.67  
    1.68  def values(fun, f):  
    1.69      return [fun(v) for v in f.values]