summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-09-24some api changesDejan Jovanović
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-22another fix for the equality class iterator Dejan Jovanović
2012-09-21Fixes for datatype dumping and printing. Add a new test case for dumping.Morgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-21better verbosity support (so it's sensible when the library is used via the API)Morgan Deters
2012-09-20map C++ exceptions to Java exceptions correctly when they are thrown, and giv...Morgan Deters
2012-09-20some bugfixes that come as a result of debugging some CASCADE/C stuff..Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-19fix subtle bug in NodeValue::toStream()Morgan Deters
2012-09-19fix for bug 370.Dejan Jovanović
2012-09-19Changing the equality engines's euivalence class iterator. Andy please check ...Dejan Jovanović
2012-09-18SMT-LIBv2 compliance regarding outputting "unknown".Morgan Deters
2012-09-17speed up option-file generation on Mac OS by an order of magnitudeMorgan Deters
2012-09-17more bindings fixesMorgan Deters
2012-09-17minor fix for models, added simple cliques option for uf strong solverAndrew Reynolds
2012-09-16enable bug regression for bug 382Morgan Deters
2012-09-16store values returned by get-value in TheoryModel::d_reps if necessary, fixes...Andrew Reynolds
2012-09-15minor interface improvements, compliance fixesMorgan Deters
2012-09-15another bindings fix (should fix debian build)Morgan Deters
2012-09-15bug testcase for model generationMorgan Deters
2012-09-14a fix for the java bindings for weiMorgan Deters
2012-09-14Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).Morgan Deters
2012-09-14Fix a few minor issues in options processing, improving usability, consistenc...Morgan Deters
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-11added getCardinality to modelAndrew Reynolds
2012-09-11Partially reverting the changes made in 4308. There is now both an Expr and N...Tim King
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback