Tianyi Liang [Fri, 27 Dec 2013 17:27:16 +0000 (11:27 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix
Morgan Deters [Fri, 27 Dec 2013 17:21:25 +0000 (12:21 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 27 Dec 2013 17:21:20 +0000 (12:21 -0500)]
Fix for ANTLR warning.
Tianyi Liang [Thu, 26 Dec 2013 23:18:26 +0000 (17:18 -0600)]
new functions in strings
Tianyi Liang [Thu, 26 Dec 2013 00:44:59 +0000 (18:44 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 25 Dec 2013 22:18:40 +0000 (17:18 -0500)]
fix for some nightly build failures
Morgan Deters [Tue, 24 Dec 2013 18:26:31 +0000 (13:26 -0500)]
Cleanup related to output language fix.
Morgan Deters [Tue, 24 Dec 2013 18:25:30 +0000 (13:25 -0500)]
Merge branch '1.3.x'
Conflicts:
NEWS
Morgan Deters [Tue, 24 Dec 2013 18:24:56 +0000 (13:24 -0500)]
Better automatic handling of output language setting.
Morgan Deters [Mon, 16 Dec 2013 14:49:05 +0000 (09:49 -0500)]
Better get-value parse error message for common user error.
Morgan Deters [Tue, 24 Dec 2013 17:45:13 +0000 (12:45 -0500)]
Minor code cleanup.
Morgan Deters [Tue, 24 Dec 2013 15:57:28 +0000 (10:57 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 3 Jun 2013 22:18:24 +0000 (18:18 -0400)]
Java datatype API fixups, datatype API examples
Morgan Deters [Mon, 23 Dec 2013 18:45:33 +0000 (13:45 -0500)]
cln now default w.r.t. build ID string
Morgan Deters [Mon, 5 Aug 2013 22:29:34 +0000 (18:29 -0400)]
Proof-checking code; fixups of segfaults and missing functionality in proof 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
Morgan Deters [Sun, 22 Dec 2013 17:06:34 +0000 (12:06 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 19 Dec 2013 16:52:00 +0000 (11:52 -0500)]
Fix to interactive mode determination.
Morgan Deters [Thu, 19 Dec 2013 16:32:56 +0000 (11:32 -0500)]
Fix option specification.
Tianyi Liang [Thu, 19 Dec 2013 18:01:28 +0000 (12:01 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Wed, 18 Dec 2013 19:27:55 +0000 (14:27 -0500)]
Merge branch '1.3.x'
[skip ci]
Morgan Deters [Wed, 18 Dec 2013 17:23:24 +0000 (12:23 -0500)]
Fix an autoconf issue with CLN in some configurations; also clarification re: license issues
[skip ci]
Morgan Deters [Wed, 18 Dec 2013 16:47:59 +0000 (11:47 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:47:50 +0000 (11:47 -0500)]
Fix configure handling for CLN (should fix win32 nightly builds)
Morgan Deters [Wed, 18 Dec 2013 16:11:36 +0000 (11:11 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:11:34 +0000 (11:11 -0500)]
Reduce autoconf version for dependence (should fix 32-bit builds).
Morgan Deters [Wed, 18 Dec 2013 16:09:41 +0000 (11:09 -0500)]
Add missing regression-results directory.
Tianyi Liang [Wed, 18 Dec 2013 02:17:12 +0000 (20:17 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Tue, 17 Dec 2013 23:56:24 +0000 (18:56 -0500)]
Merge branch '1.3.x'
Morgan Deters [Tue, 17 Dec 2013 23:56:19 +0000 (18:56 -0500)]
configure --with-portfolio disables CLN.
Tianyi Liang [Tue, 17 Dec 2013 23:52:40 +0000 (17:52 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Tue, 17 Dec 2013 22:14:45 +0000 (17:14 -0500)]
Merge branch '1.3.x'
Conflicts:
COPYING
NEWS
Morgan Deters [Tue, 17 Dec 2013 17:40:50 +0000 (12:40 -0500)]
some config changes: new --bsd option, readline gives warning, default build is now production.
Morgan Deters [Thu, 12 Dec 2013 23:24:54 +0000 (18:24 -0500)]
First attempt at incorporating LFSC proof checker into CVC4.
Morgan Deters [Mon, 16 Dec 2013 19:34:44 +0000 (14:34 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 19:34:38 +0000 (14:34 -0500)]
Send Travis-CI emails to everyone
Morgan Deters [Mon, 16 Dec 2013 14:52:52 +0000 (09:52 -0500)]
Merge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 12:30:06 +0000 (07:30 -0500)]
Fix for bug 544.
Tianyi Liang [Sun, 15 Dec 2013 17:51:44 +0000 (11:51 -0600)]
resolve merge issue.
Tianyi Liang [Sun, 15 Dec 2013 17:49:17 +0000 (11:49 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
NEWS
Morgan Deters [Sat, 14 Dec 2013 00:46:06 +0000 (19:46 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:46:01 +0000 (19:46 -0500)]
Another fix for clang.
Morgan Deters [Sat, 14 Dec 2013 00:12:54 +0000 (19:12 -0500)]
Merge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:12:31 +0000 (19:12 -0500)]
Fix stack size on in-tree regressions.
Morgan Deters [Fri, 13 Dec 2013 23:53:13 +0000 (18:53 -0500)]
cleanup
Morgan Deters [Fri, 13 Dec 2013 23:25:48 +0000 (18:25 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 23:25:36 +0000 (18:25 -0500)]
Fix link error when using clang.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 22:12:37 +0000 (17:12 -0500)]
Merge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 22:11:54 +0000 (17:11 -0500)]
Travis-CI configuration.
Morgan Deters [Fri, 13 Dec 2013 15:41:37 +0000 (10:41 -0500)]
Some minor cleanup.
Morgan Deters [Wed, 11 Dec 2013 04:43:02 +0000 (23:43 -0500)]
Update NEWS.
Morgan Deters [Wed, 11 Dec 2013 04:39:58 +0000 (23:39 -0500)]
Merge branch '1.3.x'
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.
Kshitij Bansal [Mon, 9 Dec 2013 19:14:46 +0000 (14:14 -0500)]
mv prp to regress1
Kshitij Bansal [Sat, 7 Dec 2013 00:05:35 +0000 (19:05 -0500)]
fix bug 542
Morgan Deters [Fri, 6 Dec 2013 23:45:41 +0000 (18:45 -0500)]
Initializing master for next version.
Morgan Deters [Fri, 6 Dec 2013 23:44:28 +0000 (18:44 -0500)]
Initializing 1.3.x branch.
Morgan Deters [Fri, 6 Dec 2013 23:40:01 +0000 (18:40 -0500)]
Cutting release 1.3.
Kshitij Bansal [Mon, 9 Dec 2013 19:18:38 +0000 (14:18 -0500)]
Merge branch '1.3.x'
Kshitij Bansal [Mon, 9 Dec 2013 19:14:46 +0000 (14:14 -0500)]
mv prp to regress1
Kshitij Bansal [Sat, 7 Dec 2013 08:30:18 +0000 (03:30 -0500)]
Merge branch '1.3.x'
Kshitij Bansal [Sat, 7 Dec 2013 00:05:35 +0000 (19:05 -0500)]
fix bug 542
Morgan Deters [Fri, 6 Dec 2013 23:45:41 +0000 (18:45 -0500)]
Initializing master for next version.
Morgan Deters [Fri, 6 Dec 2013 23:44:28 +0000 (18:44 -0500)]
Initializing 1.3.x branch.
Morgan Deters [Fri, 6 Dec 2013 23:40:01 +0000 (18:40 -0500)]
Cutting release 1.3.
Tianyi Liang [Fri, 6 Dec 2013 02:22:13 +0000 (20:22 -0600)]
disable substring in default mode
Morgan Deters [Thu, 5 Dec 2013 23:47:29 +0000 (18:47 -0500)]
Fix NodeValue bitfields for 32-bit; fix comment.
Morgan Deters [Thu, 5 Dec 2013 20:07:39 +0000 (15:07 -0500)]
Minor cleanup.
Morgan Deters [Thu, 5 Dec 2013 20:04:30 +0000 (15:04 -0500)]
Update copyrights, add missing file-level documentation; fix perms.
Morgan Deters [Thu, 5 Dec 2013 17:54:40 +0000 (12:54 -0500)]
Fixes related to parametric datatype printing.
Morgan Deters [Thu, 5 Dec 2013 19:07:47 +0000 (14:07 -0500)]
Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).
Morgan Deters [Thu, 5 Dec 2013 19:40:18 +0000 (14:40 -0500)]
Script fixes; when determining authorship of source files, don't count copyright-updating commits.
Morgan Deters [Thu, 5 Dec 2013 19:52:37 +0000 (14:52 -0500)]
Fix NEWS.
Morgan Deters [Thu, 5 Dec 2013 19:36:14 +0000 (14:36 -0500)]
NEWS reorganization.
Morgan Deters [Wed, 4 Dec 2013 22:26:56 +0000 (17:26 -0500)]
Remove a regression for which the portfolio takes forever (see bug 542).
Morgan Deters [Wed, 4 Dec 2013 21:45:23 +0000 (16:45 -0500)]
Minor cleanup.
Morgan Deters [Wed, 4 Dec 2013 19:16:24 +0000 (14:16 -0500)]
Partial kind branch merge, including new --rewrite-apply-to-const feature.
Morgan Deters [Wed, 4 Dec 2013 21:04:14 +0000 (16:04 -0500)]
Don't put define-funs in model output; bug 411 testcase no longer relevant.
Morgan Deters [Wed, 4 Dec 2013 19:15:27 +0000 (14:15 -0500)]
Updated acknowledgments.
Morgan Deters [Wed, 4 Dec 2013 05:50:57 +0000 (00:50 -0500)]
More Java bindings fixes
Tianyi Liang [Wed, 4 Dec 2013 04:55:57 +0000 (22:55 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 4 Dec 2013 04:53:02 +0000 (22:53 -0600)]
adds LB strategy
Tianyi Liang [Wed, 4 Dec 2013 04:53:02 +0000 (22:53 -0600)]
adds LB strategy
Morgan Deters [Wed, 4 Dec 2013 01:49:39 +0000 (20:49 -0500)]
Some fixes for swig warnings.
Tianyi Liang [Tue, 3 Dec 2013 23:05:58 +0000 (17:05 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 3 Dec 2013 23:03:34 +0000 (17:03 -0600)]
Last version for undelayed LB
Tianyi Liang [Tue, 3 Dec 2013 23:03:34 +0000 (17:03 -0600)]
Last version for undelayed LB
Morgan Deters [Tue, 3 Dec 2013 20:40:00 +0000 (15:40 -0500)]
Work around a swig segfault issue when building on Mac OS
projects / cvc5.git / log