klee/klee — pull request #181 by rsas (2014-12-02 23:34:53+00:00)
Title: Print nested let-abbreviations in ExprSMTLIBPrinter

This patch introduces nested ``let``-abbreviations in the ``ExprSMTLIBPrinter`` to reduce the size of the SMTLIBv2 queries and the corresponding processing time (bugfix for #170).

The current implementation of the ``let`` abbreviation mode does not consider expression intra-dependencies and prints all abbreviations in the same ``let`` scope. For a (simplified) example, it prints

``(assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) )``.

This is extremely inefficient if the expressions (and there many of these!) extensively reuse their subexpressions. Therefore, it's better to print the query with nested ``let``-expressions by reusing existing expression bindings in the new ``let`` scope:

``(assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) )``.

This patch adds a new function ``ExprSMTLIBPrinter::scanBindingExprDeps()`` that scans bindings for expression dependencies. The result is a vector of new bindings (``orderedBindings``) that represents the expression dependency tree.

When printing in the ``let``-abbreviation mode, the new code starts with abbreviating expressions that have no dependencies and then gradually makes these new bindings available in the upcoming ``let``-scopes where expressions with dependencies reuse them.

The effect of nested ``let``-abbreviations is comparable to ``:named`` abbreviations. However, the latter mode is not supported by the majority of the solvers.