I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, *The algorithm I want should produce a random assignment of variables to values (a substitution) such that applying the substitution to the given predicate yields a true statement. In the UNSAT case I just need to know that it is UNSAT.It is probably important to clarify what I mean by random. I think a sufficient definition is that there might be an extra parameter that acts as a seed. If I give a different seed the algorithm should give me a very different solution rather than the same solution. Frankly I'm not sure how to cash this out but it much the same way that a typical random number generator generates an integer between X and Y (well with a modulus and an addition anyhow) I'd like to generate to a wider class of predicates.I would like to use existing SMT solvers ideally in either Haskell or the JVM stack (more ideally Haskell however). I have thought of basically just randomizing the DPLL algorithm and translating the SMT problems into SAT my self but that sounds like a terrible idea when really good existing SMT solvers exist. 
Using SMT solvers to generate random solutions to given predicate
functional programming;nondeterminism;smt solvers
Let $\varphi(x)$ be the SMT instance, so the task is to find $x$ such that $\varphi(x)$ is true.One approach is to fix a hash function $h$ that maps a value of $x$ to an element of some small set $S$.  Then, you randomly select a value $s \in S$, and ask your SMT solver to find a satisfying assignment for the formula $\varphi(x) \land h(x)=s$.If you want to generate $k$ random satisfying assignments to $\varphi(x)$, you might choose $S$ to have size a bit bigger than $k$; that will probably suffice.You probably want to make the hash function $h$ as simple as possible.  There is a tradeoff between a simpler hash function (easier for the SMT solver to find satisfying assignments to $\varphi(x) \land h(x)=s$) and a better hash function that mixes the bits better (leads to more random solutions $x$).  In practice, often surprisingly simple hash functions suffice.  For instance, sometimes your hash function can be chosen via the following simple procedure: pick a random subset of the variables in $x$, project to just those variables, and then hash those variables in some simple way.  The hash function itself can be a relatively simple function, e.g., a random linear function: for example, select a random boolean matrix and multiply it with the bit vector obtained from $x$, so that $h(x)=Mx$ for some boolean matrix $M$). There may be other ways to do it, but this is one way that allows you to use an existing SMT solver, unmodified, as a black box.