diff options
author | Raimondas Sasnauskas <rsas@cs.utah.edu> | 2014-12-02 12:59:27 -0700 |
---|---|---|
committer | Raimondas Sasnauskas <rsas@cs.utah.edu> | 2014-12-12 13:37:42 -0700 |
commit | 41e56526a598316c634d29e5ef56aa71c9e38a05 (patch) | |
tree | 232048d8bafce377a4d08da3bd5ea05a02a8e9e6 /include | |
parent | 3ab04308ff9bf756284a773137254fe0240d2cab (diff) | |
download | klee-41e56526a598316c634d29e5ef56aa71c9e38a05.tar.gz |
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.
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 48d300eb..a27d2bbc 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -223,6 +223,11 @@ protected: /// emitted, so it may be used. BindingMap bindings; + /// An ordered list of expression bindings. + /// Exprs in BindingMap at index i depend on Exprs in BindingMap at i-1. + /// Exprs in orderedBindings[0] have no dependencies. + std::vector<BindingMap> orderedBindings; + /// Output stream to write to llvm::raw_ostream *o; @@ -287,6 +292,11 @@ protected: /// the usedArrays vector. void scan(const ref<Expr> &e); + /// Scan bindings for expression intra-dependencies. The result is written + /// to the orderedBindings vector that is later used for nested expression + /// printing in the let abbreviation mode. + void scanBindingExprDeps(); + /* Rules of recursion for "Special Expression handlers" and *printSortArgsExpr() * |