[SMT-LIB] Should the SMT-LIB standard be extended with a ( get-free-variables ) command?

[Martin Brain]

On Wed, 2016-01-27 at 12:13 +0000, Laar, P.J.L.J. (Pierre) van de wrote:
> Dear SMT-LIB members,
> 
> I would like that the SMT-LIB standard is extended with a ( get-free-variables ) command.
> Therefore, I have the following two questions to all SMT-LIB members:
> 
> ·        Are there more users of SMT problem solvers that would like this kind of functionality?
> 
> ·        Are there SMT problem solvers that already can provide this kind of functionality?
> 
> 
> And, of course, I will explain why I want a ( get-free-variables ) command.
> Many applications, like testing and architectural analysis, require a random solution to a particular, possibly incrementally defined, problem.

At the risk of distracting the discussion : is getting the free
variables the best / the only / a necessary step in achieving this?
Would it be more useful and give solver authors more freedom to instead
have "get random model" functionality, via an option, command or
something else?

>  One might obtain a solution by sampling all variables according to their distributions and then checking whether the sampled variable values solve the problem. However, in problems with many variables and constraints the chance of obtaining a solution in this way is extremely low. For example, the chances of randomly drawing two integer variables a and  b that satisfy the assertion (= a b) is slim.

So what is required is to find if there are solutions and then return a
randomly chosen solution based on a distribution over the input
variables.

> Currently, SMT problem solvers are no alternatives, since these problem solvers are deterministic algorithms that will always produce the same solution for a problem.

Ummm... many authors out a lot of effort in to making them deterministic
but I don't think SMT-LIB actually requires it and many have a random
seed so they can easily be made 'less deterministic'.

>  For example, for the problem with the single assertion (> x 10), a SMT problem solver will always produce the same solution, e.g., (= x 11). I assume that SMT problem solvers already internally maintain information on the free variables (see footnote 1) while solving the problem. I would like that problem solvers return this information on the free variables of a problem to the user. Given the free variables, one can sample in this subspace, for example, by adding true bins assertions (see footnote 2) to them. In this way, one can find random solutions fast and efficiently.

Over the past few years there has been some interesting work on uniform
sampling of models in SAT solvers.  Often this is used in #SAT solvers
to produce approximate model counts.  It something like this should be
possible for SMT solvers, in fact, it may have already been done, links
anyone?

Cheers,
 - Martin