about summary refs log tree commit diff homepage
path: root/lib/SMT/SMTParser.cpp
AgeCommit message (Collapse)Author
2017-02-13Removing unused lib/SMT directoryCristian Cadar
2016-11-23Renamed .pc to .kquery (kleaver query)Eric Rizzi
2015-02-22Added factory method for Arrays + hid constructors from outside callsEric Rizzi
The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made.
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.
2009-07-15Code to answer satisfiability queries.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75735 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Use a builder in the SMT parser instead of constructing expressionsCristian Cadar
directly. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75323 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Report an error in the SMT parser when encountering the few operatorsCristian Cadar
not supported yet: bvneg, bvsmod, bvxnor, rotate_left, rotate_right, repeat. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75319 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Removed debug info.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75313 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added support for not, zero_extend, and sign_extend to the SMTLIB parser.Cristian Cadar
Added support for n-ary and, or and xor. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75299 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-08Added support for bitvector variables to the SMTLIB parser (currentlyCristian Cadar
widths have to be multiples of 8). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74990 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-02Added support for bitvector constants to the SMTLIB parser. OnlyCristian Cadar
variable and array support left. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74690 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Recognizing more SMTLIB expressions (bitwise, etc.). Some of themCristian Cadar
still need to actually be constructed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74169 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-25Added support for flets.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74167 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-24Added support for LET expressions. Added simple environment supportCristian Cadar
to SMTParser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74055 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Changed SMTParser to return the parsed QueryCommand.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73277 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-12Removed parser_temp.h. Adapted the code to use SMTParser directly. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73215 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Wrote a new SMTParser that inherits from klee::expr::Parser.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73165 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-04 20:50:51 +0000