about summary refs log tree commit diff homepage
path: root/lib/SMT
AgeCommit message (Expand)Author
2015-02-22Added factory method for Arrays + hid constructors from outside callsEric Rizzi
2014-05-29Avoid non-explicit use of functions from std namespace in KLEEMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
2009-07-15Code to answer satisfiability queries.Cristian Cadar
2009-07-11Use a builder in the SMT parser instead of constructing expressionsCristian Cadar
2009-07-11Report an error in the SMT parser when encountering the few operatorsCristian Cadar
2009-07-10Removed debug info.Cristian Cadar
2009-07-10Fixed order of offsets in Extract.Cristian Cadar
2009-07-10Added support for not, zero_extend, and sign_extend to the SMTLIB parser.Cristian Cadar
2009-07-08Added support for bitvector variables to the SMTLIB parser (currentlyCristian Cadar
2009-07-02Added support for bitvector constants to the SMTLIB parser. OnlyCristian Cadar
2009-06-25Recognizing more SMTLIB expressions (bitwise, etc.). Some of themCristian Cadar
2009-06-25Added support for flets.Cristian Cadar
2009-06-25Simplified grammar by properly factoring out the rule for optional annotations.Cristian Cadar
2009-06-24Added support for LET expressions. Added simple environment supportCristian Cadar
2009-06-16Added support for comparison and arithmetic expressions.Cristian Cadar
2009-06-16Added bitvector function/predicate names to the lexer.Cristian Cadar
2009-06-16Added support for logical formulas in the SMTLIB parser.Cristian Cadar
2009-06-13Removed bits of grammar dealing with quantifiers.Cristian Cadar
2009-06-13Support for parsing SMTLIB headers. Cristian Cadar
2009-06-13Changed SMTParser to return the parsed QueryCommand.Cristian Cadar
2009-06-12Removed parser_temp.h. Adapted the code to use SMTParser directly. Cristian Cadar
2009-06-12Removed unused file.Cristian Cadar
2009-06-10Updated the SMT test driver. Other small changes to parser_temp.h andCristian Cadar
2009-06-10Removed CVC3's Parser class. Cristian Cadar
2009-06-10Wrote a new SMTParser that inherits from klee::expr::Parser.Cristian Cadar
2009-06-10Added a temporary driver to test the parser.Cristian Cadar
2009-06-10Changed expression nodes to be ExprHandle (instead of ExprHandle*), andCristian Cadar
2009-06-09Do not compile SMT parser by default. Removed automatically generatedCristian Cadar
2009-06-09Made expression nodes int the SMT parser be pointers to ExprHandle.Cristian Cadar
2009-06-09Quick hack to build SMT LLVM style.Daniel Dunbar
2009-06-09Remove exception.h and parser_exception.hDaniel Dunbar
2009-06-09Kill off uses of C++ exceptions.Daniel Dunbar
2009-06-09Remove lang.h again.Daniel Dunbar
2009-06-09Get rid of Parser language member, we only use SMTLIB.Daniel Dunbar
2009-06-09Revert r73105, I think I was too hasty in killing this.Daniel Dunbar
2009-06-09Fix a compiler warningDaniel Dunbar
2009-06-09Remove lang.h, it is unused.Daniel Dunbar
2009-06-08Made the SMTLIB parser compile. Commented out most of the grammar inCristian Cadar
2009-06-08More changes needed to make the SMTLIB parser compile.Cristian Cadar
2009-06-08Removed ValidityChecker field from ParserTemp. Temporarily replacedCristian Cadar
2009-06-08Removed support for the PL and Lisp languages.Cristian Cadar
2009-06-08Added CVC3's parser for the SMT-LIB grammar. Cristian Cadar
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 08:26:32 +0000