about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Expand)Author
2009-06-16Add basic constant folding / simplification for Eq.Daniel Dunbar
2009-06-16Add (very) basic constant folding for And,Or,Xor.Daniel Dunbar
2009-06-16Add (very) basic constant folding for Mul.Daniel Dunbar
2009-06-16Added support for comparison and arithmetic expressions.Cristian Cadar
2009-06-16Start SimplifyingExprBuilderDaniel Dunbar
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-15Support partial folding for Sub in new constant folding builder.Daniel Dunbar
2009-06-15Support partial folding for Add in new constant folding builder.Daniel Dunbar
2009-06-14Rename FoldingExprBuilder -> SimplifyingExprBuilderDaniel Dunbar
2009-06-14Kill off ExtractExpr::createByteOff.Daniel Dunbar
2009-06-14The expansion for Read{MSB,LSB} needs to continue to use the folding methods,Daniel Dunbar
2009-06-14Use ExprBuilder for constructing expressions in the Parser.Daniel Dunbar
2009-06-14Remove the (A < constant) => (A == 0 || A == 1 ... || A == constant - 1)Daniel Dunbar
2009-06-14Add ExprBuilder base class, and start of implementations.Daniel Dunbar
2009-06-14More ConstantExpr cleanup.Daniel Dunbar
2009-06-14Fail with an exec error on large (> 64-bit) floating point ops.Daniel Dunbar
2009-06-14Remove some unused functionality.Daniel Dunbar
2009-06-14More ConstantExpr tweaks.Daniel Dunbar
2009-06-14Change AddressSpace::resolveOne to take a ConstantExpr directly (and to allowDaniel Dunbar
2009-06-14Add ConstantExpr::{getLimitedValue,getZExtValue}.Daniel Dunbar
2009-06-14Rewrite ImpliedValue to use ConstantExpr operations.Daniel Dunbar
2009-06-14Add several ConstantExpr utility functions and move clients over.Daniel Dunbar
2009-06-14Add constant folding operations to ConstantExpr.Daniel Dunbar
2009-06-13Switch to using constant arrays for non-symbolic objects.Daniel Dunbar
2009-06-13Reverted last change that added createIff. Since we only handleCristian Cadar
2009-06-13Create new ObjectState constructor for explicitly creating symbolic objects.Daniel Dunbar
2009-06-13Fix for the issue reported and diagnosed by Seungbeom, where KLEE wasCristian Cadar
2009-06-13Added a helper function to construct IFF expressions.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-10Move declaration of vc_DeleteExpr outside of function.Daniel Dunbar
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-10(Missed save) Move Array construction out of MemoryObject into ObjectState.Daniel Dunbar
2009-06-10Move Array construction out of MemoryObject into ObjectState.Daniel Dunbar
2009-06-10Change ExecutionState::symbolics to include both the MemoryObject and theDaniel Dunbar
2009-06-10Use Arrays instead of MemoryObject where possible.Daniel Dunbar
2009-06-10Fix a bug in the logging solver which was printing the expression in aDaniel Dunbar
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-09More constant Array support.Daniel Dunbar
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-09Add initial support for constant Arrays.Daniel Dunbar
2009-06-09Remove Array::object.Daniel Dunbar
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 17:48:14 +0000