cvc5.git
2010-10-27 Christopher... Modifying getType to use a non-recursive algorithm...
2010-10-27 Morgan Detersfix test Makefile
2010-10-27 Morgan Deters"make dist" fixes; a distribution tarball can now build...
2010-10-27 Morgan Deterssupport focus on a particular subpackage (e.g. "expr")
2010-10-27 Morgan Detersinter-package dependence graph generation (in dot format)
2010-10-26 Morgan DetersGetValueCommand now gives a TUPLE as output, with the...
2010-10-26 Christopher... Cleaning up some header files
2010-10-26 Christopher... Adding dependency info to README
2010-10-25 Morgan Detersfor static linking of driver binary, list libmain.a...
2010-10-25 Morgan Detersmissing case in expr output; resolves bug 226
2010-10-24 Christopher... Adding unit test for InteractiveShell
2010-10-24 Morgan Detersadd a CVC4_UNDEFINED keyword, for intentionally undefin...
2010-10-23 Tim KingRemoved slack.h, and arith_activity.h. Replaced IsBasic...
2010-10-23 Christopher... Adding Parser::setInput and using it in InteractiveShel...
2010-10-22 Morgan Detersremoving unused functionality from util; related to...
2010-10-22 Morgan Detersfix valgrind-reported errors in parser builder; a non...
2010-10-22 Christopher... Saving state between lines in interactive mode (Fixes...
2010-10-22 Christopher... Using Options in ParserBuilder and InteractiveShell
2010-10-22 Christopher... Merging main/getopt.cpp, main/usage.h, and smt/options...
2010-10-22 Tim KingCode cleanup for TheoryArith.
2010-10-22 Morgan Deterscomment out the "interactive" check in SmtEngine::getVa...
2010-10-22 Tim KingFixes to getValue for TheoryArith.
2010-10-21 Christopher... * Option --no-type-checking now disables type checks...
2010-10-20 Christopher... Changing --no-early-type-checking to --no-type-checking
2010-10-20 Christopher... Enabling semantic checks in ParserBuilder
2010-10-20 Christopher... Adding detection of TTY vs. piped input for interactive...
2010-10-20 Christopher... Fixing minor whitespace bug in the parser
2010-10-20 Christopher... Adding support for interactive mode
2010-10-20 Morgan Detersfix bug #220 (assertion fails if no query/check-sat...
2010-10-14 Tim KingFixed computation of infinitesimals for arithmetic...
2010-10-13 Tim KingRemoved vector<Monomial> monos from Polynomial. Now...
2010-10-13 Tim KingAdded test/regress/regress1/arith and populated it...
2010-10-12 Morgan Deterswith --stats, statistics are dumped for memouts and...
2010-10-12 Tim KingIDENTITY has been removed.
2010-10-12 Morgan Detersminor unit test fix-ups
2010-10-12 Morgan Detersfix debugPrintNode(), debugPrintTNode(), debugPrintNode...
2010-10-12 Morgan Detersfix some leaks in parser, add debug code to node manage...
2010-10-12 Morgan Detershooked up "we are incomplete" flag after conversation...
2010-10-12 Morgan DetersMerge from cc-memout branch. Here are the main points
2010-10-12 Morgan Deterscheck last result in (get-assignment); some context...
2010-10-11 Morgan Detersuse "forward" headers
2010-10-10 Morgan Detersadditional model gen and SMT-LIBv2 compliance work...
2010-10-09 Morgan Detersreverting some changes to parser from last commit
2010-10-09 Morgan Deterssupport for SMT-LIBv2 :named attributes, and attributes...
2010-10-09 Morgan Detersfix to unit tests
2010-10-09 Morgan Detersbug fixes to model gen
2010-10-09 Morgan DetersModel generation for arith, boolean, and uf theories via
2010-10-08 Morgan Deters* (define-fun...) now has proper type checking in non...
2010-10-08 Morgan Deterssupport (set-info) on status, source, category, difficu...
2010-10-07 Morgan Detersoops, reverting a change to a regression test that...
2010-10-07 Morgan Deterstype checking for define-fun in production builds;...
2010-10-07 Morgan DetersNodeSelfIterator implementation and unit test (resolves...
2010-10-07 Tim KingSmall tableau optimization.
2010-10-07 Morgan DetersSMT-LIBv2 (define-fun...) command now functional; does...
2010-10-06 Morgan Detersdeclare-sort, define-sort working but not thoroughly...
2010-10-05 Morgan Detersparser and core support for SMT-LIBv2 commands get...
2010-10-04 Morgan Detersfix gdb issues (at least for static builds); resolves...
2010-10-04 Morgan Detersfix regular expressions in build system
2010-10-04 Morgan Detersfixing CLN builds, which had broken the build tonight...
2010-10-04 Morgan Detersre-add a dependency to fix compile warnings
2010-10-04 Morgan Detersremove/shuffle some #include dependencies; fix some...
2010-10-04 Tim KingFix to bug 211. ArithVar is now typedefed to uint32_t.
2010-10-03 Morgan Detersfile header documentation regenerated with contributors...
2010-10-02 Morgan Detersrevert a workaround fix to CDMap that was committed...
2010-10-02 Morgan Detersdump statistics on abnormal output: unexpected exceptio...
2010-10-02 Tim Kingbranches/arith-indexed-variables merged into the main...
2010-10-01 Morgan Detersre-add no-deprecated to C sources; update some file...
2010-10-01 Morgan Deterslast update broke the parser inadvertently, fixing...
2010-10-01 Morgan Detersreplacement implementation for clock_gettime() on mac...
2010-09-30 Morgan Detersfixed a number of problems with mac os x builds. build...
2010-09-28 Morgan Detersfix predicate bug in UF; code cleanup in theory.cpp
2010-09-28 Morgan Detersnode iterator work
2010-09-28 Morgan Detersfix pre-registration of operator, previously committed...
2010-09-28 Morgan Detersfix unit test for kinded iterators in Node/TNode
2010-09-28 Morgan Detersfix TLS support for platforms (e.g. Mac OS X) where...
2010-09-28 Morgan Deterscomment fix as per this morning's meeting; also, don...
2010-09-27 ACSYSadd workaround for systems (i.e., Mac OS X) that don...
2010-09-27 Tim King- This update adds DynamicArray<T>. This is a bare...
2010-09-24 Dejan Jovanovićequality triggers for the equality engine
2010-09-24 Morgan Detersroll back an unintended change with r900
2010-09-24 Morgan DetersFix build system for Mac OS X builds (resolves bug...
2010-09-24 Dejan Jovanovićbasic union find for bitvectors
2010-09-22 Christopher... Fixing NodeBuilderBlack
2010-09-21 Christopher... Rm'ing automatic type check in NodeBuilder for vars...
2010-09-21 Morgan Detersremove assertion in TNode destructor and ensure all...
2010-09-21 Morgan Detersfix statistics-registry-related memory leaks
2010-09-21 Morgan Deterspart of review (bug #197): coding conventions, file...
2010-09-21 Morgan Deterssvn:ignore properties for new bv stuff
2010-09-21 Morgan Deterssome code cleanup, documentation, review of "kinded...
2010-09-21 Dejan Jovanovićiterators for tim, begin<PLUS>() and end<PLUS>() should...
2010-09-21 Christopher... Rm'ing Makefile.in's
2010-09-21 Christopher... Moving automatic type check to NodeBuilder (Fixes:...
2010-09-20 Dejan Jovanovićhooking up the bitvector tests
2010-09-20 Dejan Jovanovićbitvector rewriting for the core theory and testcases
2010-09-16 Tim KingBug fix to CVC4::theory::arith::VarList as well as...
2010-09-14 Tim King* added test/regress/regress0/arith for easy arithmetic...
2010-09-14 Morgan Detersensure uf/congruence closure debugging stuff isn't...
2010-09-13 Morgan Detersmake Node iterators more STL-friendly, resolves bug...
2010-09-13 Morgan Detersbuild system consistency in target names for unit test...
2010-09-13 Morgan Detersstatistics are now printed on timeout (SIGXCPU) and...
next