summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2010-07-06Don't eagerly collect zombies. This should speed up things for competition b...Morgan Deters
2010-07-04make dist && make distcheck functional, other fixesMorgan Deters
2010-07-03With this commit come a number of changes to build system to supportMorgan Deters
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-07-02* Added white-box TheoryEngine test that tests the rewriterMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-29add --default-expr-depth=N command line parameter, expose setdepth() to publi...Morgan Deters
2010-06-29* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"Morgan Deters
2010-06-18bug fix (unreported on bugzilla): skolem variables failing removal from poolMorgan Deters
2010-06-16This commit just contains miscellaneous arithmetic cleanup.Tim King
2010-06-15fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)Morgan Deters
2010-06-15remove warnings about unknown #pragma GCC diagnostic on older compilersMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-06-03* Added NodeBuilder<>::getChild() to make interface more consistentMorgan Deters
2010-06-03resolving bug 139: metaKindOf() warnings still exist, but it's probably a g++...Morgan Deters
2010-06-01Fixing test failures in production buildChristopher L. Conway
2010-06-01Fixed a bug in partial_model.cpp where the data was immediately deallocated b...Tim King
2010-06-01Fixing failing test in r521Christopher L. Conway
2010-05-31First draft implementation of mkAssociativeChristopher L. Conway
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ...Tim King
2010-05-27fix bug #134: infinite deallocation loopMorgan Deters
2010-05-27Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential...Morgan Deters
2010-05-27Adding debug assertions on most TNode operationsChristopher L. Conway
2010-05-27Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)Christopher L. Conway
2010-05-21Small fixes to TheoryArith. Added a hack to make Integers a subtype of Real....Tim King
2010-05-19Significant revision to theory/arith. The new draft has a lot of small bug f...Tim King
2010-05-13Minor refactorings and corrections to commentsChristopher L. Conway
2010-05-12Adding class Smt2 to handle declaration of logic and theory symbolsChristopher L. Conway
2010-05-06fixing the nightly failure. TypeCheckingException is now marked with CVC4_PUBLICDejan Jovanović
2010-05-05bug fixes for types, old unit tests for types work nowDejan Jovanović
2010-05-04Adding general support for SMT2 set-info commandChristopher L. Conway
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-05-03theory detection fixes; fixes build breakage when you delete build directoriesMorgan Deters
2010-05-02smt parser for bit-vectorsDejan Jovanović
2010-05-01Fix for the last night's build errors (type that broke proper expression gene...Dejan Jovanović
2010-04-30Fix for bug 115, mapping was going in the wrong direction.Dejan Jovanović
2010-04-29Added the capability to construct expressions by passing the operator instead...Dejan Jovanović
2010-04-29First draft implementation of SMT v2 parserChristopher L. Conway
2010-04-28adding integer and real types to the public interfaceDejan Jovanović
2010-04-26Some cleanup. Also added the integer and real types.Dejan Jovanović
2010-04-26Adding the intermediary TypeNode to represent (and separate) the Types at the...Dejan Jovanović
2010-04-15Implementing missing NodeBuilder::constructNodeChristopher L. Conway
2010-04-15Enhancements to NodeManager tests, taking advantage of new Type implementationChristopher L. Conway
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-14* Better dependency tracking for unit test building and linking, andMorgan Deters
2010-04-13Merging from branches/decl-scopes (r401:411)Christopher L. Conway
2010-04-13Doxygen fixesChristopher L. Conway
2010-04-09added experimental "make lcov" target (it runs only unit tests); better cover...Morgan Deters
2010-04-06* Add some protected ContextObj accessors for ContextObj-derived classes:Morgan Deters
2010-04-05Adding black-box tests for NodeManager (Closes bug #65)Christopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback