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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
