projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2010-06-30 Christopher... Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UF... commit | commitdiff | tree
2010-06-30 Christopher... Adding documentation for --strict-parsing (Closes:... commit | commitdiff | tree
2010-06-30 Morgan Detersfix to switch fall-through; stats now off by default... commit | commitdiff | tree
2010-06-30 Morgan Deterschecking in CC module interface for reference. commit | commitdiff | tree
2010-06-30 Morgan DetersSupport for failing .smt and .smt2 regressions (and... commit | commitdiff | tree
2010-06-30 Morgan Deters* theory "tree" rewriting implemented and works commit | commitdiff | tree
2010-06-29 Morgan Detersadd --default-expr-depth=N command line parameter,... commit | commitdiff | tree
2010-06-29 Tim KingThis commit merges the decaying-rows branch into the... commit | commitdiff | tree
2010-06-29 Tim KingUpdate to stats.h is now back into the trunk. The... commit | commitdiff | tree
2010-06-29 Tim KingMerging the unate-propagator branch into the trunk... commit | commitdiff | tree
2010-06-29 Morgan Deters* Add CDMap<>::insertAtContextLevelZero(k, d) for inser... commit | commitdiff | tree
2010-06-24 Tim KingAdded post_mortem.py a statistics collector for user... commit | commitdiff | tree
2010-06-22 Tim KingMade ~Stat() virtual. Added some additional statistics... commit | commitdiff | tree
2010-06-18 Morgan Deters"statistics" and "staticbinary" are now tags on the... commit | commitdiff | tree
2010-06-18 Tim KingMerging the statistics branch into the main trunk.... commit | commitdiff | tree
2010-06-18 Morgan Detersbug fix (unreported on bugzilla): skolem variables... commit | commitdiff | tree
2010-06-17 Morgan Detersfix some minor annoyances in the regression test Makefi... commit | commitdiff | tree
2010-06-16 Tim KingAdded the experimental. +bool TheoryArith::AssertEquali... commit | commitdiff | tree
2010-06-16 Tim KingMore assorted changes to arithmetic in preparation... commit | commitdiff | tree
2010-06-16 Tim KingThis commit just contains miscellaneous arithmetic... commit | commitdiff | tree
2010-06-15 Morgan Detersfix last commit gcc options (-wunknown-pragmas ==>... commit | commitdiff | tree
2010-06-15 Morgan Detersremove warnings about unknown #pragma GCC diagnostic... commit | commitdiff | tree
2010-06-15 Tim KingI made a documentation change to get() to make explicit... commit | commitdiff | tree
2010-06-15 Morgan Deters(minor) fix for file documentation commit | commitdiff | tree
2010-06-14 Christopher... Adding array select/store to SMT v1 and v2 parsers commit | commitdiff | tree
2010-06-14 Tim KingFix to arith to make sure it only attempts to report... commit | commitdiff | tree
2010-06-14 Clark BarrettStarted work on array theory commit | commitdiff | tree
2010-06-06 Tim KingSome assorted fixes and local optimizations for theory... commit | commitdiff | tree
2010-06-06 Tim KingAdding += and *= to Rational. commit | commitdiff | tree
2010-06-04 Tim KingChanged how assignments are saved during check. These... commit | commitdiff | tree
2010-06-04 Tim KingChanged several arguments to const references. commit | commitdiff | tree
2010-06-04 Christopher... Adding QF_SAT to SMT parsers commit | commitdiff | tree
2010-06-04 Christopher... Reimplementing AntlrInputStream::newStreamInputStream commit | commitdiff | tree
2010-06-04 Morgan Deters** Don't fear the files-changed list, almost all change... commit | commitdiff | tree
2010-06-04 Christopher... Missing files in last commit commit | commitdiff | tree
2010-06-04 Christopher... Enabling RDL/IDL in SMT v1 and adding some simple tests commit | commitdiff | tree
2010-06-03 Christopher... Implementing input from stdin (Fixes: #144) commit | commitdiff | tree
2010-06-03 Tim KingFixes 2 issues with assignments. The first is construct... commit | commitdiff | tree
2010-06-03 Tim KingAdds toString to DeltaRational commit | commitdiff | tree
2010-06-03 Tim KingFixes a bug where registration occurs before preregistr... commit | commitdiff | tree
2010-06-03 Christopher... Changing ANTLR3 detection in configure (Fixes #147) commit | commitdiff | tree
2010-06-03 Morgan Deters* Added NodeBuilder<>::getChild() to make interface... commit | commitdiff | tree
2010-06-03 Morgan Detersresolving bug 139: metaKindOf() warnings still exist... commit | commitdiff | tree
2010-06-02 Morgan Detersadded a handful of debugTagIsOn("context") checks to... commit | commitdiff | tree
2010-06-02 Morgan Detersmore VERBOSE test failures commit | commitdiff | tree
2010-06-01 Christopher... Fixing test failures in production build commit | commitdiff | tree
2010-06-01 Tim KingThis commit adds a debugTagIsOn() guard around some... commit | commitdiff | tree
2010-06-01 Tim KingThis commit is a fix for a bug in removeITEs(). The... commit | commitdiff | tree
2010-06-01 Christopher... Adding SMT v2 parsing support for: QF_IDL, QF_NIA,... commit | commitdiff | tree
2010-06-01 Christopher... Checking for executable permission on antlr3 script commit | commitdiff | tree
2010-06-01 Tim KingFixed a bug in partial_model.cpp where the data was... commit | commitdiff | tree
2010-06-01 Christopher... Fixing failing test in r521 commit | commitdiff | tree
2010-06-01 Dejan JovanovićIn order for splitting on demand to be able to retract... commit | commitdiff | tree
2010-05-31 Christopher... First draft implementation of mkAssociative commit | commitdiff | tree
2010-05-29 Tim KingAdding a couple of example from fuzzsmt to regress1. commit | commitdiff | tree
2010-05-29 Tim KingCouple of fixes to theory arith. pivotAndUpdate now... commit | commitdiff | tree
2010-05-29 Tim KingAfter blasting the disjuncts, TheoryEngine rewrite... commit | commitdiff | tree
2010-05-28 Tim KingThis update enables TheoryArith to accept assertions... commit | commitdiff | tree
2010-05-28 Tim KingBug fixes for combining coefficients of rewritten nodes. commit | commitdiff | tree
2010-05-28 Tim KingAdded printModel() to src/theory/arith/partial_model... commit | commitdiff | tree
2010-05-28 Tim KingA few changes to the organization of TheoryEngine rewri... commit | commitdiff | tree
2010-05-28 Tim KingMoving the ITE removal from CnfStream to TheoryEngine... commit | commitdiff | tree
2010-05-27 Morgan Detersfix bug #134: infinite deallocation loop commit | commitdiff | tree
2010-05-27 Morgan Deterssmall cosmetic change to tests summary output commit | commitdiff | tree
2010-05-27 Morgan DetersRemove isAtomic() as per 4/27/2010 meeting. Add commen... commit | commitdiff | tree
2010-05-27 Morgan Detersfix compiler comparison-signedness warnings commit | commitdiff | tree
2010-05-27 Tim KingReverting this file to not include any comments. (Morga... commit | commitdiff | tree
2010-05-27 Morgan Detersadded the ability to add custom expected stdout, stderr... commit | commitdiff | tree
2010-05-27 Tim KingPreregistration has been turned on. Highly experimental... commit | commitdiff | tree
2010-05-27 Morgan DetersUse the newer automake test driver "parallel-tests... commit | commitdiff | tree
2010-05-27 Christopher... Adding debug assertions on most TNode operations commit | commitdiff | tree
2010-05-27 Christopher... Adding NodeManager::prepareToBeDestroyed() (Fixes:... commit | commitdiff | tree
2010-05-27 Christopher... Adding .cvc4_config to .gitignore commit | commitdiff | tree
2010-05-27 Morgan Detersfix bug #111: errors in building lcov-all commit | commitdiff | tree
2010-05-27 Morgan Detersfix bug 120; competition mode regression failures for... commit | commitdiff | tree
2010-05-26 Tim King . '+Outstanding case split in theory arith' commit | commitdiff | tree
2010-05-26 Christopher... Adding CnfStreamBlack tests for all Boolean connectives commit | commitdiff | tree
2010-05-26 Christopher... Fixing test failures in CnfStreamBlack (it was the... commit | commitdiff | tree
2010-05-26 Christopher... Adding documentation to my-configure commit | commitdiff | tree
2010-05-26 Christopher... Fixing my-configure commit | commitdiff | tree
2010-05-26 Christopher... Adding contrib/my-configure commit | commitdiff | tree
2010-05-26 Christopher... Adding CnfStream unit tests commit | commitdiff | tree
2010-05-26 Morgan DetersCDMap<> and CDOmap<> fixes to resolve bug 123 commit | commitdiff | tree
2010-05-26 Tim KingFix for bug 131. Added some additional debugging assert... commit | commitdiff | tree
2010-05-26 Morgan DetersCDMap: fix bug 130 commit | commitdiff | tree
2010-05-26 Christopher... Prevent lexer errors being raised if a parser error... commit | commitdiff | tree
2010-05-25 Tim KingAdded Rational constructors that only take a numerator... commit | commitdiff | tree
2010-05-25 Dejan JovanovićSome initial changes to allow for lemmas on demand. commit | commitdiff | tree
2010-05-21 Tim KingSmall fixes to TheoryArith. Added a hack to make Integ... commit | commitdiff | tree
2010-05-20 Tim KingAdded the division symbol to the parser, and minimal... commit | commitdiff | tree
2010-05-19 Tim KingSignificant revision to theory/arith. The new draft... commit | commitdiff | tree
2010-05-14 Christopher... Adding debugging code in PropEngine/CnfStream commit | commitdiff | tree
2010-05-14 Christopher... Adding ITE tests commit | commitdiff | tree
2010-05-14 Christopher... Adding rudimentary ITE handling in CnfStream commit | commitdiff | tree
2010-05-14 Christopher... Virtualizing interface between CnfStream and SatSolver commit | commitdiff | tree
2010-05-13 Christopher... Minor refactorings to PropEngine, SatSolver commit | commitdiff | tree
2010-05-13 Christopher... Minor refactorings and corrections to comments commit | commitdiff | tree
2010-05-12 Christopher... Adding ParserBuilder, reducing visibility of Parser... commit | commitdiff | tree
2010-05-12 Christopher... true and false are only defined if the core theory... commit | commitdiff | tree
2010-05-12 Christopher... Refactoring parser tests commit | commitdiff | tree
next