A python framework for Optimal Planning Modulo Theories.

This thesis is concerned with the problem of generating optimal plans for
numeric planning domains with action costs. Solving these
problems efficiently requires a seamless integration between
propositional and numeric reasoning. To this end, the candidate
will leverage recent advances in general-purpose automated reasoning 
and implement a domain-independent optimal theory-planner.

To kickstart this work, the candidate will be given a prototypical
implementation of an OMT-based planner written in Python 2.

About the current implementation:

The planner takes as input planning problems written in PDDL
(https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language),
compiles them into SMTLib (http://smtlib.cs.uiowa.edu/) formulas 
and feeds them to nuZ, an optimizing SMT solver (i.e., OMT solver).

Parsing of PDDL domains is done using a python module taken
from the Temporal Fast Downward planning system
(http://gki.informatik.uni-freiburg.de/tools/tfd/).

Construction of SMTLib formulas and solving is done using 
the python API of nuZ (http://z3prover.github.io/api/html/index.html)

Tasks of the candidate will include:

- converting the parsing module from Python 2 to Python 3;

- refactoring/improving the compilation into SMTLib
  (namely, improve the way we traverse the parsed objects
  in the current implementation);

- replace solver specific calls that are currently done
  using the Z3 Python APIs with solver-agnostic API's of
  pySMT (https://github.com/pysmt/pysmt);
  
- IMPORTANT: pySMT currently does not support optimization,
  so one task of the candidate will include extending pySMT
  with wrappers for optimizing solvers (e.g. nuZ, optimathsat, SMT-RAT);

- perform experiments on well-known benchmarks from the 
  planning literature to assess strengths and weaknesses
  of different solvers on numeric domains.