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

[Delcypher]

Hi,

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.



My plan is to write wrapper scripts to make these solver appear to "behave"
in a uniform way so that KLEE only has to parse the output of (get-value)
in one particular format. I have a few questions related to this

1) What is the correct way to ask for values of arrays (assuming that the
assertions are satisfiable)? I've been trying two different ways

* 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) )

CVC3 doesn't seem to support (get-value) and CVC4 doesn't output anything
useful. For example CVC4's response to   (get-value (unnamed unnamed_1))
was ...
(unnamed (store (store (store (...) (...) (...)) (_ bv2 32) (select (...)
(...))) (_ bv3 32) (select unnamed (_ bv3 32))))
(unnamed_1 (store (store (store (...) (...) (...)) (_ bv2 32) (select (...)
(...))) (_ bv3 32) (select unnamed_1 (_ bv3 32))))

* Asking for the value of each array element individually like so...
 (get-value ((select unnamed_1 (_ bv0 32) ) ) )
(get-value ((select unnamed_1 (_ bv1 32) ) ) )
(get-value ((select unnamed_1 (_ bv2 32) ) ) )
(get-value ((select unnamed_1 (_ bv3 32) ) ) )
(get-value ((select unnamed (_ bv0 32) ) ) )
(get-value ((select unnamed (_ bv1 32) ) ) )
(get-value ((select unnamed (_ bv2 32) ) ) )
(get-value ((select unnamed (_ bv3 32) ) ) )

Z3 and SONOLAR gave useful output that could be parsed e.g.

sat
(((select unnamed_1 (_ bv0 32) ) #x18))
(((select unnamed_1 (_ bv1 32) ) #xff))
(((select unnamed_1 (_ bv2 32) ) #xff))
(((select unnamed_1 (_ bv3 32) ) #xff))
(((select unnamed (_ bv0 32) ) #x00))
(((select unnamed (_ bv1 32) ) #x00))
(((select unnamed (_ bv2 32) ) #x00))
(((select unnamed (_ bv3 32) ) #x00))

although Z3 gave array element values in #x format and SONOLAR gave values
in the #b format. Again CVC4's response wasn't anything useful which was...
(let ((_let_0 (select unnamed_1 (_ bv0 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed_1 (_ bv1 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed_1 (_ bv2 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed_1 (_ bv3 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed (_ bv0 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed (_ bv1 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed (_ bv2 32)))) (_let_0 _let_0))
(let ((_let_0 (select unnamed (_ bv3 32)))) (_let_0 _let_0))

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.

Thanks for taking the time to read this.

Regards,
Dan Liew.














[1] http://klee.llvm.org/
[2] http://www.doc.ic.ac.uk/~dsl11/get-value-test.smt2