Constraints as Control

paper ps   
We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates constraint and imperative programming by using constraints as an advanced control structure; the developers use the monadic 'for' construct to iterate over the solutions of constraints or branch on the existence of a solution. The constructs we introduce have simple semantics that can be understood as explicit enumeration of values, but are implemented more efficiently using symbolic reasoning. Kaplan programs can manipulate constraints at run-time, with the combined benefits of type-safe syntax trees and first-class functions. The language of constraints is a functional subset of Scala, supporting arbitrary recursive function definitions over algebraic data types, sets, maps, and integers. Our implementation runs on a platform combining a constraint solver with a standard virtual machine. For constraint solving we use an algorithm that handles recursive function definitions through fair function unrolling and builds upon the state-of-the art SMT solver Z3. We evaluate Kaplan on examples ranging from enumeration of data structures to execution of declarative specifications. We found Kaplan promising because it is expressive, supporting a range of problem domains, while enabling full-speed execution of programs that do not rely on constraint programming.

Citation

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. Constraints as control. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), 2012.

BibTex Entry

@inproceedings{KoeksalETAL12ConstraintsControl,
  author = {{Ali Sinan} K\"oksal and Viktor Kuncak and Philippe Suter},
  title = {Constraints as Control},
  booktitle = {ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)},
  abstract = {
We present an extension of Scala that supports constraint
programming over bounded and unbounded domains. The
resulting language, Kaplan, provides the benefits of
constraint programming while
preserving the existing features of Scala. Kaplan integrates
constraint and imperative programming by using constraints
as an advanced control structure; the developers
use the monadic 'for' construct to iterate over the
solutions of constraints or branch on the existence of a
solution.  
The constructs we introduce have simple 
semantics that can be understood as explicit
enumeration of values, but are implemented more efficiently using
symbolic reasoning.

Kaplan programs can manipulate constraints at run-time, with the combined benefits
of type-safe syntax trees and first-class functions.
The language of constraints is
a functional subset of Scala, supporting arbitrary recursive
function definitions over algebraic data types, sets, maps, 
and integers.

Our implementation runs on a platform
combining a constraint solver with a standard virtual
machine. For constraint solving we use an algorithm that
handles recursive function definitions through
fair function unrolling and builds upon 
the state-of-the art SMT solver Z3.
We evaluate Kaplan on examples ranging
from enumeration of data structures to execution of
declarative specifications.
We found Kaplan promising
because it is expressive, supporting a range of problem domains,
while enabling full-speed execution
of programs that do not rely on constraint programming.
},
  year = 2012
}