about summary refs log tree commit diff homepage
path: root/lib/SMT
AgeCommit message (Collapse)Author
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-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-12Removed unused file.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73214 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-10Removed CVC3's Parser class. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73166 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
2009-06-10Added a temporary driver to test the parser.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73155 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-09Do not compile SMT parser by default. Removed automatically generatedCristian Cadar
parser files: We really don't want SVN to keep track of changes in these files while working on the parser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73132 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-09Quick hack to build SMT LLVM style.Daniel Dunbar
- I don't want to make proper bison/flex rules, and eventually I think we should just check in the generated files since we don't expect them to change, so for now just build the files in the src directory. Eventually we will want to disable these rules so that it works for people who don't have bison/flex. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73121 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-09Kill off uses of C++ exceptions.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73110 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove lang.h again.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73109 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Get rid of Parser language member, we only use SMTLIB.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73108 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Revert r73105, I think I was too hasty in killing this.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73107 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Fix a compiler warningDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73106 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove lang.h, it is unused.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73105 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-08More changes needed to make the SMTLIB parser compile.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73063 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Removed ValidityChecker field from ParserTemp. Temporarily replacedCristian Cadar
Expr with void* to quickly get some compilable parser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73062 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Removed support for the PL and Lisp languages.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73060 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-26 17:18:39 +0000