Automated synthesis of stochastic computational elements using decision procedures