* Replaced Monosat().init() and Monosat().setOutputFile() with Monosa…

…t().newSolver in the python api

* Removed obsolete python based file output

examples/python/color_maze.py

@@ -56,7 +56,7 @@ def verbose(s, level):
 
 print( "GRID_SIZE: %d" % GRID_SIZE )
 
-Monosat().init("-no-decide-theories")
+Monosat().newSolver("-no-decide-theories")
 
 # the graph representing the terrain grid
 graph = Graph()

examples/python/maxflow_benchmark.py

@@ -39,7 +39,7 @@ def pairwise(iterable):
     args.seed = random.randint(1,1000000)
 print("Random seed: %d"%(args.seed))
 random.seed(args.seed)
-Monosat().init("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
+Monosat().newSolver("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
 g= Graph()
 
 source = g.addNode()

examples/python/reach_benchmark.py

@@ -38,7 +38,7 @@ def pairwise(iterable):
     args.seed = random.randint(1,1000000)
 print("Random seed: %d"%(args.seed))
 random.seed(args.seed)
-Monosat().init("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
+Monosat().newSolver("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
 g= Graph()
 
 grid = dict()

examples/python/shortestpath_benchmark.py

@@ -39,7 +39,7 @@ def pairwise(iterable):
     args.seed = random.randint(1,1000000)
 print("Random seed: %d"%(args.seed))
 random.seed(args.seed)
-Monosat().init("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
+Monosat().newSolver("-verb=1 -rnd-seed=%d -theory-order-vsids -vsids-both %s   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf "%(args.seed, "-decide-theories" if args.decide_theories else "-no-decide-theories" ))
 g= Graph()
 
 grid = dict()

examples/python/test_acyclic.py

@@ -12,8 +12,8 @@
 print("RandomSeed=" + str(seed))
 
 size =6
-filename="/tmp/test.gnf"
-#Monosat().init("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
+
+#Monosat().newSolver("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
 
 
 

examples/python/test_bv_ite.py

@@ -7,10 +7,9 @@
 
 random.seed(seed)
 print("RandomSeed=" + str(seed))
-filename="/tmp/test.gnf"
-Monosat().init("""-debug-learnts=/tmp/test_learnts.cnf -decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf """)
 
-print("Writing file to " + filename)
+Monosat().newSolver("""-debug-learnts=/tmp/test_learnts.cnf -decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf """)
+
 
 bv1 = BitVector(4)
 bv2 = BitVector(4)

examples/python/test_maxflow_bv.py

@@ -9,7 +9,7 @@
 print("RandomSeed=" + str(seed))
 
 
-Monosat().init("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
+Monosat().newSolver("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
 
 
 

examples/python/test_maxflow_pb.py

@@ -9,9 +9,7 @@
 print("RandomSeed=" + str(seed))
 
 
-filename="/tmp/test_bv"
-
-Monosat().init("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
+Monosat().newSolver("-decide-graph-bv -no-decide-theories -no-decide-graph-rnd   -lazy-maxflow-decisions -conflict-min-cut -conflict-min-cut-maxflow -reach-underapprox-cnf ")
 
 
 

examples/routing/router.py

@@ -51,7 +51,7 @@ def route(filename, monosat_args,use_maxflow=False, draw_solution=True):
     if(len(monosat_args)>0):
         args = " ".join(monosat_args)
         print("MonoSAT args: " + args)
-        Monosat().init(args)
+        Monosat().newSolver(args)
 
     g = Graph()
 

examples/routing/router_multi.py

@@ -66,7 +66,7 @@ def route_multi(filename, monosat_args, maxflow_enforcement_level, flowgraph_sep
     if (len(monosat_args) > 0):
         args = " ".join(monosat_args)
         print("Monosat args: " + args)
-        Monosat().init(args)
+        Monosat().newSolver(args)
 
     if draw_solution:
         #the dicts here are only used to print the solution at the end. Disable for benchmarking.