cvc5.git
2012-02-23 Morgan Deterspcvc4 only built if --with-portfolio given to the confi...
2012-02-22 Tim KingFix for bug 305.
2012-02-22 Morgan Detersfixes to configure and boost.m4 to make certain boost...
2012-02-22 Morgan Detersanother static library unavailability issue
2012-02-22 Morgan Detersmake sure to clear out READLINE_LIBS if readline causes...
2012-02-22 Morgan DetersAdded OutputChannel::propagateAsDecision() functionalit...
2012-02-22 Morgan DetersFixes to documentation / fixes for MacOS
2012-02-22 Kshitij Bansalminor change to order fn in sat solver's ElimLt
2012-02-21 Morgan Detersadd a "--with-portfolio" configure option that makes...
2012-02-21 Morgan Detersfix src/util/hash.h to specialize GNU's hash template...
2012-02-21 Morgan Deterslanguage bindings fixes for yesterday's portfolio merge
2012-02-21 Dejan JovanovićFix for bug303. The problem was with function applicati...
2012-02-21 Morgan Detersdon't require libboost_thread (its presence is detected...
2012-02-20 Morgan Detersfix sharing issue for portfolio (full lit-to-node map...
2012-02-20 Morgan Detersfix "make dist"
2012-02-20 Morgan Deterszlib not required; remove configure's dependency on it
2012-02-20 Morgan Detersportfolio merge
2012-02-20 Morgan Detersreadline links in -ltermcap -ltinfo too (fixes breakage...
2012-02-20 Morgan DetersAdded Theory::postsolve() infrastructure as Clark reque...
2012-02-20 Morgan DetersBy default, ONLY enable symmetry breaker ONLY for QF_UF...
2012-02-16 Morgan Detersclarify wording in README, thanks for finding this...
2012-02-16 Tim KingLast commit accidentally lacked r2778 and r2779 from...
2012-02-15 Tim KingThis commit merges into trunk the branch branches/arith...
2012-02-13 François Bobotprecision in theoryskel
2012-02-13 Morgan Detersproper handling of improper get-value
2012-02-12 Morgan Deterscopyright year updated to 2012
2012-02-12 Morgan Detersseparate new-theory components into a "theoryskel"...
2012-02-11 Morgan Detersensure using bash for new-theory script
2012-02-10 Morgan Detersattempt at a fix for the local regression failure ...
2012-02-10 Morgan Detersscript to ease creating a new theory from scratch ...
2012-02-10 Morgan Deterscorrect comment typo found during today's architectural...
2012-02-09 Dejan Jovanovićfixing antoher small bug in backtracking
2012-02-08 Dejan Jovanovićfixing a bug in uf_engine application lookup backtracking
2012-02-08 Tim KingNumber of changes to cvc_printer.cpp. Specialized the...
2012-02-07 Morgan Detersre-adding comment about available languages
2012-02-07 Dejan Jovanovićremoving the 100 integer benchmarks from regress0,...
2012-02-07 Dejan Jovanovićfixing some missing stuff
2012-02-06 Tim KingFixing a bug in the integer unit tests when configured...
2012-02-05 Dejan Jovanovićchanges to the cvc4 language printer, so that it actual...
2012-02-04 Andrew Reynoldssupport for isWellFounded/mkGroundTerm on uninterprette...
2012-02-03 Dejan Jovanovićupdating configure to use python-config for building...
2012-01-27 Morgan Deterseffecting the same change in the compat Java binding...
2012-01-25 Tim KingAdding regress1 test ooo.rf6.smt2.
2012-01-23 Tim KingPartial fix to TheoryEngine::getExplanation so that...
2012-01-23 Dejan Jovanovićfix for bug295
2012-01-17 Andrew Reynoldsupdates to smt2 parser to support datatypes, minor...
2011-12-15 Tim KingPartial fix to bug 295.
2011-12-15 Tim KingFix to the previous commit.
2011-12-15 Tim KingPartial fix in arithmetic for propagating shared terms...
2011-12-14 Andrew Reynoldsadded minor documentation for parametric datatypes...
2011-12-14 Morgan Detersminor fixes to printing and parsing of CVC-language...
2011-12-14 Dejan Jovanovićsome more bug fixes (TNode -> Node, normalize literals...
2011-12-12 Dejan Jovanović* merging some uf stuff from incremental_work branch...
2011-12-10 Dejan Jovanovićadding additional checks for theories propagating liter...
2011-12-10 Dejan Jovanovića bit more changes, when propagting equalities/dis...
2011-12-10 Dejan Jovanovićattempt to fix bug 293: if a split on a trivial shared...
2011-12-08 Morgan DetersDisable a BV rewriter statistic (after checking with...
2011-12-06 Morgan DetersLemmaStatus changes, as agreed to during 12/2 meeting.
2011-12-06 Morgan Detersoops, removing some integer operations that leaked...
2011-12-06 Morgan Detersfix errors in smt-lib2 output; needed for debugging
2011-12-05 Morgan Deterschange short-circuiting behavior of Command execution...
2011-12-02 Morgan DetersError detection is different now---with new Command...
2011-11-30 Morgan Detersdisable bug288.smt so that "make check" goes through...
2011-11-30 Morgan Detersfix linking errors on oneiric
2011-11-30 Tim KingSimplified bug288.smt to reflect the problem in integer...
2011-11-30 Tim KingAdded a failing regression test corresponding to bug...
2011-11-30 Tim KingAdding a failing UFLIA benchmark corresponding to bug...
2011-11-29 Tim KingMerging the branch branches/arithmetic/shared-terms...
2011-11-26 Morgan DetersFix Java JNI installation path
2011-11-22 Morgan Detersfix module name for CVC4 jar file; part of the fix...
2011-11-22 Morgan DetersMore language bindings work:
2011-11-16 Morgan DetersFix "make dist". Fixes to python and ruby bindings...
2011-11-16 Morgan DetersAddressed many of the concerns raised in the public...
2011-11-16 Morgan Detersfix to build system for java bindings
2011-11-16 Morgan Deters* Applying Andy's fix for datatypes bug #286; thanks...
2011-11-15 Morgan DetersBindings work (ocaml bindings are now sort of working...
2011-11-15 Morgan Detersadditional minor changes to get python binding on bette...
2011-11-15 Morgan Detersfixes for python language binding, added python example
2011-11-14 Morgan Deterspublic tests need to be linked against gmp/cln explicit...
2011-11-06 Morgan Detersdatatype stuff in compatibility interface implemented
2011-11-05 Morgan DetersContext::ScopedPush implemented (in support of theory...
2011-11-04 Morgan DetersSTRING_TYPE and CONST_STRING and associate type infrast...
2011-11-02 Morgan DetersOnly print a shortlist of most-commonly-used options...
2011-11-02 Morgan Detersgive an option error if the user specifies --proof...
2011-11-02 Morgan Detersfully implement the always-check-again-after-the-output...
2011-11-02 Morgan DetersSometimes antlr decides to generate lexers and parsers...
2011-11-02 Morgan Detersbetter Integer asserts when there's overflow on convers...
2011-11-01 Morgan DetersImprovements to header installation on user machines...
2011-10-31 Morgan Detersfixes to assertions in GMP to match CLN behavior
2011-10-31 Tim KingAdded assertions to the CLN implementation of Integer...
2011-10-31 Morgan Detersanother make distclean fix
2011-10-31 Morgan Detersfixes to "make distclean" and "make maintainerclean"
2011-10-31 Morgan Detersfix to "make install"
2011-10-29 Morgan Detersfix some doxygen warnings
2011-10-29 Morgan Deterssupport for proof regressions in other parts of the...
2011-10-29 Morgan Detersfix unit tests
2011-10-29 Morgan DetersSupport for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF...
2011-10-28 Morgan Detersproof regressions
2011-10-28 Morgan Deters* ability to output NodeBuilders without first converti...
2011-10-28 Liana Hadareanmerged the proofgen3 branch into trunk:
next