index
:
~cnx/klee
this commit
1.0.x
1.1.x
1.2.x
1.3.x
1.4.x
2.0.x
2.1.x
2.2.x
2.3.x
3.0.x
master
psychic
svcomp
svcomp_32bit
KLEE fork for patch differentiation testing
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
/
SMT
Age
Commit message (
Expand
)
Author
2009-07-10
Fixed order of offsets in Extract.
Cristian Cadar
2009-07-10
Added support for not, zero_extend, and sign_extend to the SMTLIB parser.
Cristian Cadar
2009-07-08
Added support for bitvector variables to the SMTLIB parser (currently
Cristian Cadar
2009-07-02
Added support for bitvector constants to the SMTLIB parser. Only
Cristian Cadar
2009-06-25
Recognizing more SMTLIB expressions (bitwise, etc.). Some of them
Cristian Cadar
2009-06-25
Added support for flets.
Cristian Cadar
2009-06-25
Simplified grammar by properly factoring out the rule for optional annotations.
Cristian Cadar
2009-06-24
Added support for LET expressions. Added simple environment support
Cristian Cadar
2009-06-16
Added support for comparison and arithmetic expressions.
Cristian Cadar
2009-06-16
Added bitvector function/predicate names to the lexer.
Cristian Cadar
2009-06-16
Added support for logical formulas in the SMTLIB parser.
Cristian Cadar
2009-06-13
Removed bits of grammar dealing with quantifiers.
Cristian Cadar
2009-06-13
Support for parsing SMTLIB headers.
Cristian Cadar
2009-06-13
Changed SMTParser to return the parsed QueryCommand.
Cristian Cadar
2009-06-12
Removed parser_temp.h. Adapted the code to use SMTParser directly.
Cristian Cadar
2009-06-12
Removed unused file.
Cristian Cadar
2009-06-10
Updated the SMT test driver. Other small changes to parser_temp.h and
Cristian Cadar
2009-06-10
Removed CVC3's Parser class.
Cristian Cadar
2009-06-10
Wrote a new SMTParser that inherits from klee::expr::Parser.
Cristian Cadar
2009-06-10
Added a temporary driver to test the parser.
Cristian Cadar
2009-06-10
Changed expression nodes to be ExprHandle (instead of ExprHandle*), and
Cristian Cadar
2009-06-09
Do not compile SMT parser by default. Removed automatically generated
Cristian Cadar
2009-06-09
Made expression nodes int the SMT parser be pointers to ExprHandle.
Cristian Cadar
2009-06-09
Quick hack to build SMT LLVM style.
Daniel Dunbar
2009-06-09
Remove exception.h and parser_exception.h
Daniel Dunbar
2009-06-09
Kill off uses of C++ exceptions.
Daniel Dunbar
2009-06-09
Remove lang.h again.
Daniel Dunbar
2009-06-09
Get rid of Parser language member, we only use SMTLIB.
Daniel Dunbar
2009-06-09
Revert r73105, I think I was too hasty in killing this.
Daniel Dunbar
2009-06-09
Fix a compiler warning
Daniel Dunbar
2009-06-09
Remove lang.h, it is unused.
Daniel Dunbar
2009-06-08
Made the SMTLIB parser compile. Commented out most of the grammar in
Cristian Cadar
2009-06-08
More changes needed to make the SMTLIB parser compile.
Cristian Cadar
2009-06-08
Removed ValidityChecker field from ParserTemp. Temporarily replaced
Cristian Cadar
2009-06-08
Removed support for the PL and Lisp languages.
Cristian Cadar
2009-06-08
Added CVC3's parser for the SMT-LIB grammar.
Cristian Cadar