[klee-dev] Named Annotations in SMT-LIB2 expressions

[Dan Liew]

Hi Srijan,

> While '--smtlib-abbreviation-mode=named' had the desired effect, I also
> wanted the mapping of expressions to emitted annotations which I believe can
> be obtained from BindingMap in lib/Expr/ExprSMTLIBPrinter.cpp.

That is correct.

> Could someone shed more light on the same/ correct me if I'm wrong and give
> me a few pointers about how the bindings work. I'll be obliged by any help
> in this regard.

To understand how the printer is used you should take a look at
ExprSMTLIBPrinter.h [1]
which is very well documented.

The named bindings work by first traversing the Expr tree looking for
expressions that can
be abbreviated before doing any printing. You should look at
ExprSMTLIBPrinter::scanAll(...) [2] and
ExprSMTLIBPrinter::printExpression(...) [3]

[1] https://github.com/klee/klee/blob/master/include/klee/util/ExprSMTLIBPrinter.h
[2] https://github.com/klee/klee/blob/master/lib/Expr/ExprSMTLIBPrinter.cpp#L435-L447
[3] https://github.com/klee/klee/blob/master/lib/Expr/ExprSMTLIBPrinter.cpp#L167-L206

Hope that helps.