cvc5.git
2011-02-13 Tim King3 heuristics were added to arithmetic. A heuristic...
2011-01-05 Dejan Jovanovićfix for build errors
2011-01-05 Dejan JovanovićCommit for the theory engine and rewriter changes....
2010-12-17 Morgan Deterstls.h, rational.h, and integer.h are only re-generated...
2010-12-16 Morgan Detersminor fixes for correct doxygen output
2010-12-14 Morgan Detersmake some CC module methods private that should not...
2010-12-14 Morgan Deterscongruence closure module now supports things other...
2010-12-14 Morgan Deterspermit PARAMETERIZED operators to be zero-ary
2010-12-14 Morgan Detersfix to static learning application in UF, resolves...
2010-11-24 Dejan JovanovićChangin the get() semantics to a CDQeue-sque semantics.
2010-11-19 Morgan DetersMerge from ufprop branch, including:
2010-11-19 Morgan Detersadd statistics support information to --show-config
2010-11-18 Morgan Deterssmall changes to documentation; also, '\''make doc...
2010-11-17 Morgan Detersfix improper CongruenceClosureWhite test by merging...
2010-11-17 Morgan Detersadd some stats to UF/CC
2010-11-17 Morgan DetersThe "UF engineering issues" release, after much profiling.
2010-11-16 Tim KingAdded Theory::presolve().
2010-11-16 Morgan DetersSmtEngine now fails with a ModalException if --incremen...
2010-11-16 Morgan Detersfix function signatures
2010-11-15 Morgan Deterscleanup from today's commits: delegate as-yet-unimpleme...
2010-11-15 Tim KingChanges to Solver and PropEngine to support lemmasOnDem...
2010-11-15 Morgan DetersPretty-printer infrastructure created (in src/printer...
2010-11-15 Tim KingThis commit merges the arith-prop-opt branch into the...
2010-11-15 Morgan Detersminor tweaks to last commit, testing infrastructure
2010-11-15 Morgan Detersfix some things with the build system (make dist, make...
2010-11-12 Dejan JovanovićSome bug fixes in the SAT for lemmas, and an experiment...
2010-11-11 Morgan Detersmake addsourcedir executable
2010-11-09 Dejan JovanovićLemmas on demand work, push-pop, some cleanup.
2010-11-08 Morgan Deterscommand-line flag to disable theory registration, also...
2010-11-08 Morgan Deterscleanup, documentation, SMT-LIBv2 compliance
2010-11-08 Morgan Detersfix out-of-date version/copyright for minisats
2010-11-05 Christopher... Moving Options fiddling to options.h
2010-11-04 Morgan Deterscompetition mode implies --no-checking
2010-11-04 Tim KingMoving the post_mortem.py script out of contrib and...
2010-11-04 Tim KingUpdates post_mortem.py script to be able to handle...
2010-11-04 Tim KingThis commit adds the ejected and un-ejected statistics.
2010-11-03 Tim KingAdds size() to RowVector.
2010-11-03 Tim KingAdds statistics for the number of Uservariables and...
2010-11-03 Tim KingAdds AverageStat to stats.h.
2010-10-31 Morgan Deterssmall fix to debug segfaults
2010-10-31 Morgan Detersenable dependence graphs in doxygen; fix lots of doxyge...
2010-10-31 Morgan Detersmaximize stack limit, handle SEGV signals on an alterna...
2010-10-30 Tim KingAdds a hueristic from Alberto's thesis. For a fixed...
2010-10-29 Tim KingFix for a problem caused by using a != instead of ...
2010-10-29 Morgan Detersportability updates to build system
2010-10-29 Tim KingAdds a very small test that triggers a bug. The bug...
2010-10-29 Morgan Detersminor fixes as a result of review of Chris's getType...
2010-10-29 Tim KingFixes RowVector::has().
2010-10-29 Tim KingFactors out the QF_LRA decision procedure from TheoryAr...
2010-10-28 Tim KingThe Row implementation has no been replaced by RowVecto...
2010-10-28 Christopher... Changing NodeBuilder::debugCheckType() to maybeCheckType()
2010-10-28 Christopher... Disabling bottom-up algorithm in NodeManager::getType...
2010-10-28 Morgan Detersfix confusing CXXTEST configure message, indicating...
2010-10-27 Christopher... Small change to documentation in NodeManager::getType
2010-10-27 Christopher... Slightly more efficient version of getType
2010-10-27 Morgan Detersmake dist-building more pleasant (put .tar.gz in builds...
2010-10-27 Christopher... Changing dependency info in README
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
next