summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-03Added 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-02Merge branch '1.3.x'Morgan Deters
2014-01-02Update copyright year.Morgan Deters
2013-12-27Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2013-12-27minor fixTianyi Liang
2013-12-27minor fixTianyi Liang
2013-12-27Merge branch '1.3.x'Morgan Deters
2013-12-27Fix for ANTLR warning.Morgan Deters
2013-12-26new functions in stringsTianyi Liang
2013-12-25Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2013-12-25fix for some nightly build failuresMorgan Deters
2013-12-24Cleanup related to output language fix.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-24Better get-value parse error message for common user error.Morgan Deters
2013-12-24Minor code cleanup.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-23cln now default w.r.t. build ID stringMorgan Deters
2013-12-23Proof-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-22Merge branch '1.3.x'Morgan Deters
2013-12-22Fix to interactive mode determination.Morgan Deters
2013-12-22Fix option specification.Morgan Deters
2013-12-19Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2013-12-18Merge branch '1.3.x'Morgan Deters
[skip ci]
2013-12-18Fix an autoconf issue with CLN in some configurations; also clarification ↵Morgan Deters
re: license issues [skip ci]
2013-12-18Merge branch '1.3.x'Morgan Deters
2013-12-18Fix configure handling for CLN (should fix win32 nightly builds)Morgan Deters
2013-12-18Merge branch '1.3.x'Morgan Deters
2013-12-18Reduce autoconf version for dependence (should fix 32-bit builds).Morgan Deters
2013-12-18Add missing regression-results directory.Morgan Deters
2013-12-17Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2013-12-17Merge branch '1.3.x'Morgan Deters
2013-12-17configure --with-portfolio disables CLN.Morgan Deters
2013-12-17Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2013-12-17Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS
2013-12-17some config changes: new --bsd option, readline gives warning, default build ↵Morgan Deters
is now production.
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-16Merge branch '1.3.x'Morgan Deters
2013-12-16Send Travis-CI emails to everyoneMorgan Deters
2013-12-16Merge branch '1.3.x'Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-15resolve merge issue.Tianyi Liang
2013-12-15Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: NEWS
2013-12-13Merge branch '1.3.x'Morgan Deters
2013-12-13Another fix for clang.Morgan Deters
2013-12-13Merge branch '1.3.x'Morgan Deters
2013-12-13Fix stack size on in-tree regressions.Morgan Deters
2013-12-13cleanupMorgan Deters
2013-12-13Merge branch '1.3.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback