about summary refs log tree commit diff homepage
path: root/lib/SMT/smtlib.y
AgeCommit message (Collapse)Author
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-10Fixed order of offsets in Extract.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75311 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-25Simplified grammar by properly factoring out the rule for optional annotations.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74165 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-16Added support for comparison and arithmetic expressions.Cristian Cadar
We need to add support for smod to Kleaver. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73459 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Added bitvector function/predicate names to the lexer.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73455 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-16Added support for logical formulas in the SMTLIB parser.Cristian Cadar
Started to work on parsing bitvector terms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73453 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Removed bits of grammar dealing with quantifiers.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73280 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-13Support for parsing SMTLIB headers. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73278 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-10Updated the SMT test driver. Other small changes to parser_temp.h andCristian Cadar
smtlib.y. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73167 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Changed expression nodes to be ExprHandle (instead of ExprHandle*), andCristian Cadar
added a quick hack to change Bison unions to structs. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73154 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Made expression nodes int the SMT parser be pointers to ExprHandle.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73131 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove exception.h and parser_exception.hDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73111 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Made the SMTLIB parser compile. Commented out most of the grammar inCristian Cadar
smtlib.y. Made a temporary functional Makefile that compiles the lex/bison generated files. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73064 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Added CVC3's parser for the SMT-LIB grammar. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73059 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-23 03:35:16 +0000