Andrew Reynolds [Sat, 4 Jan 2014 04:36:55 +0000 (22:36 -0600)]
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Andrew Reynolds [Fri, 3 Jan 2014 18:13:13 +0000 (12:13 -0600)]
Added support for proof production in Equality Engine. Cleaned up existing 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.
Morgan Deters [Thu, 2 Jan 2014 19:13:17 +0000 (14:13 -0500)]
Merge branch '1.3.x'
Morgan Deters [Thu, 2 Jan 2014 19:13:08 +0000 (14:13 -0500)]
Update copyright year.
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.
projects / cvc5.git / log