title: Custom simplifiers
body: <p>Back in the old days (ie. last year), we used to be able to use theory plugins as a hack to implement custom simplifiers. The Z3 doc even contained <a href="http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/group__theory__plugin__ex.html" rel="nofollow">an example of "procedural attachments"</a>.</p>
  
  <p>My question is very simple; is there any way to achieve the same goal with Z3 4.x?</p>
  
  <p>In particular, I'm interested in a way to provide Z3 with externally computed evaluations for ground terms.</p>