Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing ↵ | Andrew Reynolds | |
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup. | |||
2014-01-02 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-02 | Update copyright year. | Morgan Deters | |
2013-12-27 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2013-12-27 | minor fix | Tianyi Liang | |
2013-12-27 | minor fix | Tianyi Liang | |
2013-12-27 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-27 | Fix for ANTLR warning. | Morgan Deters | |
2013-12-26 | new functions in strings | Tianyi Liang | |
2013-12-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2013-12-25 | fix for some nightly build failures | Morgan Deters | |
2013-12-24 | Cleanup related to output language fix. | Morgan Deters | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: NEWS | |||
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-24 | Better get-value parse error message for common user error. | Morgan Deters | |
2013-12-24 | Minor code cleanup. | Morgan Deters | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
2013-12-23 | cln now default w.r.t. build ID string | Morgan Deters | |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line | |||
2013-12-22 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-22 | Fix to interactive mode determination. | Morgan Deters | |
2013-12-22 | Fix option specification. | Morgan Deters | |
2013-12-19 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2013-12-18 | Merge branch '1.3.x' | Morgan Deters | |
[skip ci] | |||
2013-12-18 | Fix an autoconf issue with CLN in some configurations; also clarification ↵ | Morgan Deters | |
re: license issues [skip ci] | |||
2013-12-18 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-18 | Fix configure handling for CLN (should fix win32 nightly builds) | Morgan Deters | |
2013-12-18 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-18 | Reduce autoconf version for dependence (should fix 32-bit builds). | Morgan Deters | |
2013-12-18 | Add missing regression-results directory. | Morgan Deters | |
2013-12-17 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2013-12-17 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-17 | configure --with-portfolio disables CLN. | Morgan Deters | |
2013-12-17 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2013-12-17 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS | |||
2013-12-17 | some config changes: new --bsd option, readline gives warning, default build ↵ | Morgan Deters | |
is now production. | |||
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-12-16 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-16 | Send Travis-CI emails to everyone | Morgan Deters | |
2013-12-16 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-16 | Fix for bug 544. | Morgan Deters | |
2013-12-15 | resolve merge issue. | Tianyi Liang | |
2013-12-15 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: NEWS | |||
2013-12-13 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-13 | Another fix for clang. | Morgan Deters | |
2013-12-13 | Merge branch '1.3.x' | Morgan Deters | |
2013-12-13 | Fix stack size on in-tree regressions. | Morgan Deters | |
2013-12-13 | cleanup | Morgan Deters | |
2013-12-13 | Merge branch '1.3.x' | Morgan Deters | |