summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-10-04disable model-generation by default in cvc3 compatibility layer. should fix ...Morgan Deters
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-10-04IllegalArgumentException in java needs to be named "CVC4IllegalArgumentExcept...Morgan Deters
2012-10-03minor fix for mbqi in finite model findingAndrew Reynolds
2012-10-03implemented collectModelInfo for TheoryBVLiana Hadarean
2012-10-03updates to contrib scripts to match docsMorgan Deters
2012-10-03better documentation, allow examples to be installed, etcMorgan Deters
2012-10-03New model code, mostly workinClark Barrett
2012-10-03new README and INSTALL filesMorgan Deters
2012-10-03added support for interrupting TheoryBVLiana Hadarean
2012-10-03--wait-to-join / --no-wait-to-join optionKshitij Bansal
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
2012-10-02workaround for a nasty CLN bugMorgan Deters
2012-10-01"Fix" (disable) portfolio when using quantifiersKshitij Bansal
2012-10-01make sure to mark LogicInfo as CVC4_PUBLICMorgan Deters
2012-10-01fix for dejan: term ITEs now dumped correctlyMorgan Deters
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-30minor changes to arithmetic assertions involving nonlinearity and models (rel...Morgan Deters
2012-09-30minor fixes to pickler (hopefully fixes Debian build from last night)Morgan Deters
2012-09-30release notesMorgan Deters
2012-09-29Calling the setIncompleteness() flag on all full checks once a non-linear ter...Tim King
2012-09-29Fix a few segfaults in driver.Morgan Deters
2012-09-29draft RELEASE-NOTES file, and minor release stuffMorgan Deters
2012-09-29fixes to "make distclean" and C compatibility bindings; should fix the broken...Morgan Deters
2012-09-29fixes to "make distclean" and C compatibility bindings; should fix the broken...Morgan Deters
2012-09-29This commit add interpretation by lemma for INTS_DIVISION, INTS_MODULUS, and ...Tim King
2012-09-28Some fixes to portfolioKshitij Bansal
2012-09-28fix distribution of cvc4_assert.iMorgan Deters
2012-09-28fixes for compatibility (i.e., CVC3) Java bindingsMorgan Deters
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-28some fixes to build systemMorgan Deters
2012-09-28fix production-build linking errorMorgan Deters
2012-09-28Public interface review items:Morgan Deters
2012-09-28* fix compatibility library naming for SMT-LIBv1Morgan Deters
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
2012-09-27finally, a portable solutionMorgan Deters
2012-09-27fix for non-MacMorgan Deters
2012-09-27speed up mkoptions script (esp. on Macs)Morgan Deters
2012-09-27better progress indicator for mkoptionsMorgan Deters
2012-09-26disable building of cvc3_george system-test object (which isn't used yet anyw...Morgan Deters
2012-09-26Finish off SEXPR kind work.Morgan Deters
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-26Fix a handful of things for Mac, and Java bindings.Morgan Deters
2012-09-26bug #398 test (bug was resolved last night), and a script to download all bug...Morgan Deters
2012-09-26Fix type checking for define-funs (resolves bug 398).Morgan Deters
2012-09-26The Tuesday Afternoon Catch-All Commit (TACAC):Morgan Deters
2012-09-25fixMorgan Deters
2012-09-25fix some Mac issuesMorgan Deters
2012-09-25some buggy examples for incrementality, and make bug326 run as part of make r...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback