Constraint Solver in Scala

by Matthias Schlaipfer for Scala Team

This GSoC project proposal is based on the idea described at http://lara.epfl.ch/w/solver. It consists of two separate goals: First, DPLL(T) solving architecture. Currently scabolic uses an imperative solving algorithm which is difficult to modify. DPLL(T) is well-established and would provide a better framework. One part of this implementation is incremental SAT solving. Second, a decision procedure to reason about functional data structures. Such a decision procedure is, for example, described in the paper "Decision procedures for algebraic data types with abstractions". Having such an implementation would, for example, allow to replace Z3 as the theory solver in Leon. It would be nice to have the complete stack written in Scala. Especially regarding certain optimizations, which are impossible with a black box solver.