about summary refs log tree commit diff homepage
path: root/lib/Expr/ExprSMTLIBPrinter.cpp
AgeCommit message (Collapse)Author
2020-11-12Casting.h: isa_and_nonnull<>Julian Büning
2020-11-12Ref: implement operator bool()Julian Büning
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr ↵Cristian Cadar
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-03-13Moved options in ExprSMTLIBPrinter.cpp to the expression building and ↵Cristian Cadar
printing category
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2017-08-27Remove unnecessary null pointer checksOscar Deits
Fixes klee/klee#717 delete on null pointer is always safe.
2017-06-12llvm: don't use clEnumValEnd for LLVM 4.0Jiri Slaby
It became unnecessary when defining options and mainly undefined. So introduce KLEE_LLVM_CL_VAL_END as suggested by @delcypher. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2015-04-15Fix the handling of AShrExpr in ExprSMTLIBPrinter so that an overshiftDan Liew
always goes to zero (matches LLVM's APInt::ashr(...)). This is meant to partially address issue #218. There are a few problems with this commit * It is possible for AShrExpr to not be abbreviated because the scan methods will not see that we print the 0th child of the AShrExpr twice * The added test case should really be run through an SMT solver ( i.e. STP) but that requires infrastructure changes.
2015-02-19Teach ExprSMTLIBPrinter to use SMTLIBv2's distinct function ratherDan Liew
than writing "(not (= a b))". This makes the code simpler and queries slightly simpler.
2014-12-13Add a few line breaks to make the code more readable inDan Liew
ExprSMTLIBPrinter
2014-12-13Clean up some ExprSMTLIBPrinter code by using llvm_unreachableDan Liew
2014-12-13Clean up a few comments in ExprSMTLIBPrinterDan Liew
2014-12-12Print nested let-abbreviations in ExprSMTLIBPrinterRaimondas Sasnauskas
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.
2014-12-02Fix typoDan Liew
2014-12-02Add a comment explaining why the query expr is being negated.Dan Liew
2014-12-02The printing of constraints and the QueryExpr have been merged into aDan Liew
single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-05-29Fix headerMartin Nowack
2014-05-29Avoid non-explicit use of functions from std namespace in KLEEMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2014-05-11Fix the logic in ExprSMTLIBPrinter::getSortPeter Collingbourne
This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those.
2014-04-02Modify the SMT-LIB printer to declare arrays in a deterministic ↵Peter Collingbourne
(alphabetical) order.
2014-03-09Use clang-format to reformat SMT-LIB printer in LLVM style.Peter Collingbourne
2013-05-08Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to ↵Cristian Cadar
negateQueryExpression() to make it clear what it does." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181445 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Nice patch by Dan Liew that adds support for printing queries in theCristian Cadar
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-17 00:23:05 +0000