Permalink
Browse files

Move ExternalCNF and ExternalXCSP to a single ExternalSolver.py

  • Loading branch information...
9thbit committed Oct 29, 2013
1 parent 745512a commit cfa26d30cfefe3b54f92e8f3a827dc9af54fedf4
View
@@ -3,7 +3,7 @@ SRC = ./src
SOL = ./solvers
# List of wrappers that need to be compiled before the solver interfaces.
-WRAPPERS = sat mip externalcnf externalxcsp
+WRAPPERS = sat mip
SOLVERS = $(wildcard $(SOL)/*)
TEMPTARGETS = $(patsubst $(SOL)/%, %, $(SOLVERS))
@@ -1,20 +0,0 @@
-include ../../make.project
-
-MAINDIR = $(shell pwd)/../..
-CURDIR ?= .
-PYTHON = $(CURDIR)/python
-
-PYFILE = $(PYTHON)/ExternalCNF.py
-
-wrapper:
-
-clean:
- rm -rf *~ $(PYTHON)/*.pyc
-
-clean_swig:
-
-install_python: wrapper
- cd $(PYTHON); python $(MAINDIR)/tools/setup.py install
-
-externalsolver_local: wrapper
- echo "asdf"
@@ -1,52 +0,0 @@
-from ExternalSolver import ExternalSolver
-from SatWrapper import SatWrapperSolver
-import Numberjack
-import datetime
-
-
-class ExternalCNFSolver(ExternalSolver, SatWrapperSolver):
-
- def __init__(self):
- # We need to call init on both parent classes, super won't do this
- # if they both inherit from base class object.
- ExternalSolver.__init__(self)
- SatWrapperSolver.__init__(self)
-
- def set_model(self, model, solver_id, solver_name, solver):
- self.model = model
- print "Outputting to:", self.filename
- SatWrapperSolver.output_cnf(self, self.filename)
-
- def parse_output(self, output):
- """
- Parses the solver output, which should conform to the output of the
- SAT Solver competitions.
- http://www.satcompetition.org/2009/format-solvers2009.html
- """
- from SatWrapper import SatWrapperIntArray
- print "c Parse output"
- values = SatWrapperIntArray()
- for line in output.split("\n"):
- line = line.strip()
- first_two = line[:2]
- if len(line) == 0:
- continue
-
- if first_two == "s ":
- if "UNSATISFIABLE" in line or "UNSAT" in line:
- self.sat = Numberjack.UNSAT
- elif "SATISFIABLE" in line or "SAT" in line:
- self.sat = Numberjack.SAT
- elif first_two == "v ":
- t = datetime.datetime.now()
- for v in map(int, line[2:].split()):
- if v != 0:
- values.add(v)
- print "time to add this value line: %.4f" % (datetime.datetime.now() - t).total_seconds()
-
- # elif first_two == "d " or first_two == "c ":
- # self.parse_solver_info_line(line[2:])
-
- t = datetime.datetime.now()
- self.store_solution(values)
- print "Time to store solution: %.4f" % (datetime.datetime.now() - t).total_seconds()
@@ -1,20 +0,0 @@
-include ../../make.project
-
-MAINDIR = $(shell pwd)/../..
-CURDIR ?= .
-PYTHON = $(CURDIR)/python
-
-PYFILE = $(PYTHON)/ExternalXCSP.py
-
-wrapper:
-
-clean:
- rm -rf *~ $(PYTHON)/*.pyc
-
-clean_swig:
-
-install_python: wrapper
- cd $(PYTHON); python $(MAINDIR)/tools/setup.py install
-
-externalsolver_local: wrapper
- echo "asdf"
@@ -1,96 +0,0 @@
-from ExternalSolver import ExternalSolver
-import Numberjack
-import sys
-
-
-class ExternalXCSPIntVariable(object):
-
- def __init__(self, nj_var):
- self.nj_var = nj_var
- self.value = None
-
- def get_value(self):
- print "ExternalXCSPIntVariable.get_value", str(self.value)
- return self.value
-
-
-class ExternalXCSPSolver(ExternalSolver):
-
- def __init__(self):
- super(ExternalXCSPSolver, self).__init__()
-
- def set_model(self, model, solver_id, solver_name, solver):
- self.model = model
- self.output_model()
-
- for nj_var, i in sorted(self.out_object.njvar_mapping.iteritems(), key=lambda (k, v): v):
- my_var = ExternalXCSPIntVariable(nj_var)
- nj_var.setVar(solver_id, solver_name, my_var, new_solver=solver)
- nj_var.solver = solver
- self.variables.append(my_var)
-
- def output_model(self):
- from XCSPOut import XCSPOutput
- self.out_object = XCSPOutput(self.model)
- self.out_object.output(self.filename)
-
- def parse_output(self, output):
- """
- Parses the solver output, which should conform to the output of the
- CSP Solver competitions. http://cpai.ucc.ie/09/
- """
- values = []
- for line in output.split("\n"):
- line = line.strip()
- first_two = line[:2]
- if len(line) == 0:
- continue
-
- if first_two == "s ":
- print line
- if "UNSATISFIABLE" in line or "UNSAT" in line:
- self.sat = Numberjack.UNSAT
- elif "SATISFIABLE" in line or "SAT" in line:
- self.sat = Numberjack.SAT
- elif first_two == "v ":
- print "Valued:", line
- values.extend(map(int, line[2:].split()))
- elif first_two == "d " or first_two == "c ":
- self.parse_solver_info_line(line[2:])
-
- if self.sat == Numberjack.SAT:
- for i, variable in enumerate(self.variables):
- print "Setting", variable, "equal to:", values[i]
- variable.value = values[i]
-
- def parse_solver_info_line(self, line):
- bits = [a.strip() for a in line.split() if len(a.strip()) > 0] # Strip additional whitespace
- for i in xrange(0, len(bits), 2):
- try:
- name, value = bits[i], bits[i + 1]
- print name, value
- if name == "NODES" or name == "NDS":
- self.nodes = int(value)
- elif name == "BACKTRACKS":
- self.backtracks = int(value)
- elif name == "CHECKS":
- self.checks = int(value)
- elif name == "FAILURES":
- self.failures = int(value)
- except Exception as e:
- print >> sys.stderr, str(e)
- pass
-
-
-class Solver(Numberjack.NBJ_STD_Solver):
- def __init__(self, model=None, X=None, FD=False, clause_limit=-1, encoding=None):
- # if X:
- # import sys
- # print >> sys.stderr, "Warning explicitly specifying the decision variables for an external CSP solver is currently not supported."
-
- # We pass an empty model to NBJ_STD_Solver to prevent it from loading
- # and trying to decompse each expression.
- Numberjack.NBJ_STD_Solver.__init__(self, "ExternalXCSP", "ExternalXCSP", None, None, FD, clause_limit, encoding)
- self.solver_id = model.getSolverId()
- self.model = model
- self.solver.set_model(model, self.solver_id, self.Library, solver=self)
View
@@ -1,8 +1,11 @@
+from SatWrapper import SatWrapperSolver
import Numberjack
import subprocess as sp
import threading
+import datetime
import signal
import atexit
+import sys
import os
@@ -97,10 +100,6 @@ def __init__(self):
self.propags = -1
self.time = -1
self.threads = 1
- self.verbosity = 0 # Currently not passed down to external solvers
- self.var_heuristic = None # Currently not passed down to external solvers
- self.val_heuristic = None # Currently not passed down to external solvers
- self.randomization = None # Currently not passed down to external solvers
# info_regexps should be a dictionary containing the attributes to parse
# from the solver's output. The dictionary key is the attribute name,
@@ -112,7 +111,18 @@ def __init__(self):
# to self.key = cast_func(group_match_str)
self.info_regexps = {}
- # Register the clean_up function to be run when python is exiting, there may be a better time for this...
+ # Currently not passed down to external solvers since we require a
+ # specific level of output to parse their output. Instead, we control
+ # the level this output we print based on this value.
+ self.verbosity = 0
+
+ # None of these are currently being passed down to external solvers:
+ self.var_heuristic = None
+ self.val_heuristic = None
+ self.randomization = None
+
+ # Register the clean_up function to be run when python is exiting, there
+ # may be a better time for this...
atexit.register(ExternalSolver.clean_up, self)
def generate_filename(self):
@@ -202,3 +212,151 @@ def getTime(self):
def printPython(self):
return repr(self)
+
+# ---------- External CNF ----------
+
+
+class ExternalCNFSolver(ExternalSolver, SatWrapperSolver):
+
+ def __init__(self):
+ # We need to call init on both parent classes, super won't do this
+ # if they both inherit from base class object.
+ ExternalSolver.__init__(self)
+ SatWrapperSolver.__init__(self)
+
+ def set_model(self, model, solver_id, solver_name, solver):
+ self.model = model
+ # print "c minimise_obj:", str(self.minimise_obj), self.minimise_obj.get_min(), self.minimise_obj.get_max()
+ # print "c maximise_obj:", str(self.maximise_obj)
+ print "c Outputting to:", self.filename
+ SatWrapperSolver.output_cnf(self, self.filename)
+
+ def parse_output(self, output):
+ """
+ Parses the solver output, which should conform to the output of the
+ SAT Solver competitions.
+ http://www.satcompetition.org/2009/format-solvers2009.html
+ """
+ from SatWrapper import SatWrapperIntArray
+ print "c Parse output"
+ values = SatWrapperIntArray()
+ for line in output.split("\n"):
+ line = line.strip()
+ first_two = line[:2]
+ if len(line) == 0:
+ continue
+
+ if first_two == "s ":
+ if "UNSATISFIABLE" in line or "UNSAT" in line:
+ self.sat = Numberjack.UNSAT
+ elif "SATISFIABLE" in line or "SAT" in line:
+ self.sat = Numberjack.SAT
+ elif first_two == "v ":
+ # t = datetime.datetime.now()
+ for v in map(int, line[2:].split()):
+ if v != 0:
+ values.add(v)
+ # print "time to add this value line: %.4f" % (datetime.datetime.now() - t).total_seconds()
+
+ # elif first_two == "d " or first_two == "c ":
+ # self.parse_solver_info_line(line[2:])
+
+ t = datetime.datetime.now()
+ self.store_solution(values)
+ print "c Time to store solution: %.4f" % (datetime.datetime.now() - t).total_seconds()
+
+
+# ---------- External XCSP ----------
+
+
+class ExternalXCSPIntVariable(object):
+
+ def __init__(self, nj_var):
+ self.nj_var = nj_var
+ self.value = None
+
+ def get_value(self):
+ print "ExternalXCSPIntVariable.get_value", str(self.value)
+ return self.value
+
+
+class ExternalXCSPSolver(ExternalSolver):
+
+ def __init__(self):
+ super(ExternalXCSPSolver, self).__init__()
+
+ def set_model(self, model, solver_id, solver_name, solver):
+ self.model = model
+ self.output_model()
+
+ for nj_var, i in sorted(self.out_object.njvar_mapping.iteritems(), key=lambda (k, v): v):
+ my_var = ExternalXCSPIntVariable(nj_var)
+ nj_var.setVar(solver_id, solver_name, my_var, new_solver=solver)
+ nj_var.solver = solver
+ self.variables.append(my_var)
+
+ def output_model(self):
+ from XCSPOut import XCSPOutput
+ self.out_object = XCSPOutput(self.model)
+ self.out_object.output(self.filename)
+
+ def parse_output(self, output):
+ """
+ Parses the solver output, which should conform to the output of the
+ CSP Solver competitions. http://cpai.ucc.ie/09/
+ """
+ values = []
+ for line in output.split("\n"):
+ line = line.strip()
+ first_two = line[:2]
+ if len(line) == 0:
+ continue
+
+ if first_two == "s ":
+ print line
+ if "UNSATISFIABLE" in line or "UNSAT" in line:
+ self.sat = Numberjack.UNSAT
+ elif "SATISFIABLE" in line or "SAT" in line:
+ self.sat = Numberjack.SAT
+ elif first_two == "v ":
+ print "Valued:", line
+ values.extend(map(int, line[2:].split()))
+ elif first_two == "d " or first_two == "c ":
+ self.parse_solver_info_line(line[2:])
+
+ if self.sat == Numberjack.SAT:
+ for i, variable in enumerate(self.variables):
+ print "Setting", variable, "equal to:", values[i]
+ variable.value = values[i]
+
+ def parse_solver_info_line(self, line):
+ bits = [a.strip() for a in line.split() if len(a.strip()) > 0] # Strip additional whitespace
+ for i in xrange(0, len(bits), 2):
+ try:
+ name, value = bits[i], bits[i + 1]
+ print name, value
+ if name == "NODES" or name == "NDS":
+ self.nodes = int(value)
+ elif name == "BACKTRACKS":
+ self.backtracks = int(value)
+ elif name == "CHECKS":
+ self.checks = int(value)
+ elif name == "FAILURES":
+ self.failures = int(value)
+ except Exception as e:
+ print >> sys.stderr, str(e)
+ pass
+
+
+# class Solver(Numberjack.NBJ_STD_Solver):
+# def __init__(self, model=None, X=None, FD=False, clause_limit=-1, encoding=None):
+# # if X:
+# # import sys
+# # print >> sys.stderr, "Warning explicitly specifying the decision variables for an external CSP solver is currently not supported."
+
+# # We pass an empty model to NBJ_STD_Solver to prevent it from loading
+# # and trying to decompse each expression.
+# Numberjack.NBJ_STD_Solver.__init__(self, "ExternalXCSP", "ExternalXCSP", None, None, FD, clause_limit, encoding)
+# self.solver_id = model.getSolverId()
+# self.model = model
+# self.solver.set_model(model, self.solver_id, self.Library, solver=self)

0 comments on commit cfa26d3

Please sign in to comment.