[SMT-LIB] Is the output of (get-value () ) standardised for Arrays?

[Alberto Griggio]

Hello Dan, 

> I'm currently working on a project to allow the use of SMTLIBv2 solvers
> that support the QF_AUFBV or QF_ABV logics in a program known as KLEE 
[1].
> 
> I've made good progress so far and I am able to generate valid SMTLIBv2
> files. Here is an example generated by KLEE [2]. For the work I'm doing 
all
> symbolic constants are arrays, for example...
> 
> (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
> 
> unnamed is the symbolic array whose values I wish to determine.
> 
> The problem I'm facing is finding a way to parse the output of a 
SMTLIBv2
> compliant solver. Parsing the response to (check-sat) is straight 
forward
> as the response can only be
> "sat|unsat|unknown". However in addition to determining whether or not 
a
> set of assertions are satisfiable, I need to determine the values of 
the
> arrays (in the example file unnamed and unnamed_1) with
> the (get-value ) command. I've been playing around with different 
solvers
> (CVC3, CVC4, MathSat5, SONOLAR, STP, Z3) and I've had limited success
> because none of the solvers give consistent output for me to parse.

> * Asking for the value of the arrays directly like so...
> 
>   (get-value (unnamed unnamed_1))
> 
>    This didn't seem to work very well. The only solver that gave a 
useful
> answer was SONOLAR in the following format...
>    (select  unnamed #b00000000000000000000000000000000) #b00011011)
> 
>    Z3 and mathsat gave answers that seem to refer to their models 
(running
> `$mathsat -model < get-value-test.smt2` shows what @1 and @0 actually 
are).
> e.g. Mathsat5's output was..
> 
>   sat
>   ( (unnamed @1)
>     (unnamed_1 @0) )

As far as I understand the SMT-LIBv2 standard, this is correct. A
response to a get-value command is required to produce "value"
terms (Section 5.1.6 of the standard, pp 61-62). "value" terms are
defined in Section 4.5.1 (page 53) to be some special, logic-specific,
ground terms. In the case of arrays, they are "abstract values" (see
http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2),
i.e. just sybmols starting with a @ character.

[...]

> 2) Is there any standard on the way bitvectors are displayed when using 
the
> (get-value ()) command?
> As above Z3 uses #x syntax, SONOLAR #b syntax and Mathsat5 (when 
invoked
> via it's command line options rather than (get-value) uses the (_ bv5 
8)
> syntax. This makes things a little difficult for me so if there is a
> "standard" I'd like to write my parser to that and have my wrapper 
scripts
> make the others solves "appear" to produce output that is in the 
"standard"
> format.

I don't think the standard says anything about this, sorry. Perhaps some
solvers have options to specify which format to use, but I'm not sure...


Best,
Alberto