title: Transpiling language constructs to z3
body: <p>I am looking for a discussion of how to convert various programming language constructs to Z3, without limiting the efficiency of the solver.</p>
  
  <p>In particular, is there an algorithm and a set of best-practice rules for converting a function/program expressed in continuation passing style to Z3?</p>
  
  <p>The use context is to use Z3 for implementing a type system for a programming language, so the solution has to be efficient and incremental (e.g. retain previous Z3 ASTs in the Z3 instance).</p>
  
  <p>I am aware of Boogie, but is looking for something more lightweight if it is possible.</p>
  
  <p>Constraining the semantics of the input language somewhat is acceptable, but not so far that it is trivially expressible in SMTLIB.</p>
  
  <p>I am basically looking for a discussion of different strategies that one might consider for various typical language constructs.</p>
  
  <p>Edit: It might be acceptable to have restrictions that make the input language non-turing-complete and only reasonable efficient for smaller program fragments (like functions in a library). E.g. the input language could be a language for writing "statically checked" libraries that is later transpiled down to libraries for an existing dynamic programming language with dynamic runtime asserts where appropriate.</p>