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

[Laar, P.J.L.J. (Pierre) van de]

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. 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.
Currently, SMT problem solvers are no alternatives, since these problem solvers are deterministic algorithms that will always produce the same solution for a problem. 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.

Thanks in advance for your answers to my two questions.

Greetings,
    Piërre van de Laar

[TNO-ESI_logo-email-signature]



Dr. Piërre van de Laar
Research Fellow





Embedded Systems Innovation by TNO
De Rondom 1, 5612 AP Eindhoven
Postbus 6235, 5600 HE  Eindhoven
The Netherlands

T   +31 8886 69388
E   pierre.vandelaar at tno.nl<mailto:pierre.vandelaar at tno.nl>
W www.esi.nl<http://www.esi.nl/>

TNO Eindhoven<http://www.tno.nl/locaties/eh>
Disclaimer<http://www.tno.nl/emaildisclaimer>



Footnote 1. To give some examples of what I consider free variables in a (single assertion) problem:
no free variable:              (= x 3)                                 => {}
                                            (or (= x 3) (= x 6) )             => {}
                                            (and (= x 6) (= y x) )          => {}

one free variable:            (= a b)                                 => {x} where x in {a,b}
(= a (+ b 5) )                       => {x} where x in {a,b}

two free variables:         (and (= k l) (= k m) (= o p) )             => {x1,x2} where x1 in {k,l,m} and x2 in {o,p}
                                            (= str (++ str1 str2) )                        => {x1,x2} a subset of the set {str,str1,str2}
                                             (= a (+ b c) )                                      => {x1,x2} a subset of the set {a,b,c}
                                            (> a b)                                                => {a,b}

Sets of three free variables:
                                            (or (= a b) (= c d) )             => { {x1,c,d} with x1 in {a,b}, {a,b,x2} with x2 in {c,d} }


Footnote 2. A true bins assertion is an assertion in which the value of a variable is explicitly restricted to a number of bins. The assertion is true, since the bins together contain all possible values. Yet, the assertion is (fortunately) not simplified by the SMT problem solver to true. As a consequence, by randomizing the order of the bins in the true bins assertion, the problem solver can still solve the original problem, yet the solution will be biased to the first/last bins based on the heuristic of the particular problem solver used. An example of a true bins assertion is:
               (or (>78 x) (< x (- 123)) (<= (- 123) x 78) )




This message may contain information that is not intended for you. If you are not the addressee or if this message was sent to you by mistake, you are requested to inform the sender and delete the message. TNO accepts no liability for the content of this e-mail, for the manner in which you use it and for damage of any kind resulting from the risks inherent to the electronic transmission of messages.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.png
Type: image/png
Size: 9674 bytes
Desc: image001.png
URL: </pipermail/smt-lib/attachments/20160127/04bab120/attachment.png>