cvc5.git
10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Thu, 26 Dec 2013 00:44:59 +0000 (18:44 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agofix for some nightly build failures
Morgan Deters [Wed, 25 Dec 2013 22:18:40 +0000 (17:18 -0500)]
fix for some nightly build failures

10 years agoCleanup related to output language fix.
Morgan Deters [Tue, 24 Dec 2013 18:26:31 +0000 (13:26 -0500)]
Cleanup related to output language fix.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 24 Dec 2013 18:25:30 +0000 (13:25 -0500)]
Merge branch '1.3.x'

Conflicts:
NEWS

10 years agoBetter automatic handling of output language setting.
Morgan Deters [Tue, 24 Dec 2013 18:24:56 +0000 (13:24 -0500)]
Better automatic handling of output language setting.

10 years agoBetter get-value parse error message for common user error.
Morgan Deters [Mon, 16 Dec 2013 14:49:05 +0000 (09:49 -0500)]
Better get-value parse error message for common user error.

10 years agoMinor code cleanup.
Morgan Deters [Tue, 24 Dec 2013 17:45:13 +0000 (12:45 -0500)]
Minor code cleanup.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 24 Dec 2013 15:57:28 +0000 (10:57 -0500)]
Merge branch '1.3.x'

10 years agoJava datatype API fixups, datatype API examples
Morgan Deters [Mon, 3 Jun 2013 22:18:24 +0000 (18:18 -0400)]
Java datatype API fixups, datatype API examples

10 years agocln now default w.r.t. build ID string
Morgan Deters [Mon, 23 Dec 2013 18:45:33 +0000 (13:45 -0500)]
cln now default w.r.t. build ID string

10 years agoProof-checking code; fixups of segfaults and missing functionality in proof generatio...
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

10 years agoMerge branch '1.3.x'
Morgan Deters [Sun, 22 Dec 2013 17:06:34 +0000 (12:06 -0500)]
Merge branch '1.3.x'

10 years agoFix to interactive mode determination.
Morgan Deters [Thu, 19 Dec 2013 16:52:00 +0000 (11:52 -0500)]
Fix to interactive mode determination.

10 years agoFix option specification.
Morgan Deters [Thu, 19 Dec 2013 16:32:56 +0000 (11:32 -0500)]
Fix option specification.

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Thu, 19 Dec 2013 18:01:28 +0000 (12:01 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 19:27:55 +0000 (14:27 -0500)]
Merge branch '1.3.x'

[skip ci]

10 years agoFix an autoconf issue with CLN in some configurations; also clarification re: license...
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]

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:47:59 +0000 (11:47 -0500)]
Merge branch '1.3.x'

10 years agoFix configure handling for CLN (should fix win32 nightly builds)
Morgan Deters [Wed, 18 Dec 2013 16:47:50 +0000 (11:47 -0500)]
Fix configure handling for CLN (should fix win32 nightly builds)

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 18 Dec 2013 16:11:36 +0000 (11:11 -0500)]
Merge branch '1.3.x'

10 years agoReduce autoconf version for dependence (should fix 32-bit builds).
Morgan Deters [Wed, 18 Dec 2013 16:11:34 +0000 (11:11 -0500)]
Reduce autoconf version for dependence (should fix 32-bit builds).

10 years agoAdd missing regression-results directory.
Morgan Deters [Wed, 18 Dec 2013 16:09:41 +0000 (11:09 -0500)]
Add missing regression-results directory.

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Wed, 18 Dec 2013 02:17:12 +0000 (20:17 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 17 Dec 2013 23:56:24 +0000 (18:56 -0500)]
Merge branch '1.3.x'

10 years agoconfigure --with-portfolio disables CLN.
Morgan Deters [Tue, 17 Dec 2013 23:56:19 +0000 (18:56 -0500)]
configure --with-portfolio disables CLN.

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Tue, 17 Dec 2013 23:52:40 +0000 (17:52 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 17 Dec 2013 22:14:45 +0000 (17:14 -0500)]
Merge branch '1.3.x'

Conflicts:
COPYING
NEWS

10 years agosome config changes: new --bsd option, readline gives warning, default build is now...
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.

10 years agoFirst attempt at incorporating LFSC proof checker into CVC4.
Morgan Deters [Thu, 12 Dec 2013 23:24:54 +0000 (18:24 -0500)]
First attempt at incorporating LFSC proof checker into CVC4.

10 years agoMerge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 19:34:44 +0000 (14:34 -0500)]
Merge branch '1.3.x'

10 years agoSend Travis-CI emails to everyone
Morgan Deters [Mon, 16 Dec 2013 19:34:38 +0000 (14:34 -0500)]
Send Travis-CI emails to everyone

10 years agoMerge branch '1.3.x'
Morgan Deters [Mon, 16 Dec 2013 14:52:52 +0000 (09:52 -0500)]
Merge branch '1.3.x'

10 years agoFix for bug 544.
Morgan Deters [Mon, 16 Dec 2013 12:30:06 +0000 (07:30 -0500)]
Fix for bug 544.

10 years agoresolve merge issue.
Tianyi Liang [Sun, 15 Dec 2013 17:51:44 +0000 (11:51 -0600)]
resolve merge issue.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sun, 15 Dec 2013 17:49:17 +0000 (11:49 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
NEWS

10 years agoMerge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:46:06 +0000 (19:46 -0500)]
Merge branch '1.3.x'

10 years agoAnother fix for clang.
Morgan Deters [Sat, 14 Dec 2013 00:46:01 +0000 (19:46 -0500)]
Another fix for clang.

10 years agoMerge branch '1.3.x'
Morgan Deters [Sat, 14 Dec 2013 00:12:54 +0000 (19:12 -0500)]
Merge branch '1.3.x'

10 years agoFix stack size on in-tree regressions.
Morgan Deters [Sat, 14 Dec 2013 00:12:31 +0000 (19:12 -0500)]
Fix stack size on in-tree regressions.

10 years agocleanup
Morgan Deters [Fri, 13 Dec 2013 23:53:13 +0000 (18:53 -0500)]
cleanup

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 23:25:48 +0000 (18:25 -0500)]
Merge branch '1.3.x'

10 years agoFix link error when using clang.
Morgan Deters [Fri, 13 Dec 2013 23:25:36 +0000 (18:25 -0500)]
Fix link error when using clang.

10 years agoFix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.

10 years agoFix to Travis-CI config.
Morgan Deters [Fri, 13 Dec 2013 23:21:01 +0000 (18:21 -0500)]
Fix to Travis-CI config.

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 13 Dec 2013 22:12:37 +0000 (17:12 -0500)]
Merge branch '1.3.x'

10 years agoTravis-CI configuration.
Morgan Deters [Fri, 13 Dec 2013 22:11:54 +0000 (17:11 -0500)]
Travis-CI configuration.

10 years agoSome minor cleanup.
Morgan Deters [Fri, 13 Dec 2013 15:41:37 +0000 (10:41 -0500)]
Some minor cleanup.

10 years agoUpdate NEWS.
Morgan Deters [Wed, 11 Dec 2013 04:43:02 +0000 (23:43 -0500)]
Update NEWS.

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 11 Dec 2013 04:39:58 +0000 (23:39 -0500)]
Merge branch '1.3.x'

10 years agoFix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.

10 years agoWhitespace.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.

10 years agoFix warning.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.

10 years agoRemove "NodeValue width" output
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output

10 years agoGLPK build identifier, license warnings.
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.

10 years agoFix timer statistics to report correct time even on process abort.
Morgan Deters [Wed, 11 Dec 2013 04:17:13 +0000 (23:17 -0500)]
Fix timer statistics to report correct time even on process abort.

10 years agoWhitespace.
Morgan Deters [Wed, 11 Dec 2013 04:16:27 +0000 (23:16 -0500)]
Whitespace.

10 years agoFix warning.
Morgan Deters [Wed, 11 Dec 2013 00:04:00 +0000 (19:04 -0500)]
Fix warning.

10 years agoRemove "NodeValue width" output
Morgan Deters [Tue, 10 Dec 2013 05:54:31 +0000 (00:54 -0500)]
Remove "NodeValue width" output

10 years agoGLPK build identifier, license warnings.
Morgan Deters [Mon, 9 Dec 2013 23:31:17 +0000 (18:31 -0500)]
GLPK build identifier, license warnings.

10 years agomv prp to regress1
Kshitij Bansal [Mon, 9 Dec 2013 19:14:46 +0000 (14:14 -0500)]
mv prp to regress1

10 years agofix bug 542
Kshitij Bansal [Sat, 7 Dec 2013 00:05:35 +0000 (19:05 -0500)]
fix bug 542

10 years agoInitializing master for next version.
Morgan Deters [Fri, 6 Dec 2013 23:45:41 +0000 (18:45 -0500)]
Initializing master for next version.

10 years agoInitializing 1.3.x branch.
Morgan Deters [Fri, 6 Dec 2013 23:44:28 +0000 (18:44 -0500)]
Initializing 1.3.x branch.

10 years agoCutting release 1.3.
Morgan Deters [Fri, 6 Dec 2013 23:40:01 +0000 (18:40 -0500)]
Cutting release 1.3.

10 years agoMerge branch '1.3.x'
Kshitij Bansal [Mon, 9 Dec 2013 19:18:38 +0000 (14:18 -0500)]
Merge branch '1.3.x'

10 years agomv prp to regress1
Kshitij Bansal [Mon, 9 Dec 2013 19:14:46 +0000 (14:14 -0500)]
mv prp to regress1

10 years agoMerge branch '1.3.x'
Kshitij Bansal [Sat, 7 Dec 2013 08:30:18 +0000 (03:30 -0500)]
Merge branch '1.3.x'

10 years agofix bug 542
Kshitij Bansal [Sat, 7 Dec 2013 00:05:35 +0000 (19:05 -0500)]
fix bug 542

10 years agoInitializing master for next version.
Morgan Deters [Fri, 6 Dec 2013 23:45:41 +0000 (18:45 -0500)]
Initializing master for next version.

10 years agoInitializing 1.3.x branch.
Morgan Deters [Fri, 6 Dec 2013 23:44:28 +0000 (18:44 -0500)]
Initializing 1.3.x branch.

10 years agoCutting release 1.3.
Morgan Deters [Fri, 6 Dec 2013 23:40:01 +0000 (18:40 -0500)]
Cutting release 1.3.

10 years agodisable substring in default mode
Tianyi Liang [Fri, 6 Dec 2013 02:22:13 +0000 (20:22 -0600)]
disable substring in default mode

10 years agoFix NodeValue bitfields for 32-bit; fix comment.
Morgan Deters [Thu, 5 Dec 2013 23:47:29 +0000 (18:47 -0500)]
Fix NodeValue bitfields for 32-bit; fix comment.

10 years agoMinor cleanup.
Morgan Deters [Thu, 5 Dec 2013 20:07:39 +0000 (15:07 -0500)]
Minor cleanup.

10 years agoUpdate copyrights, add missing file-level documentation; fix perms.
Morgan Deters [Thu, 5 Dec 2013 20:04:30 +0000 (15:04 -0500)]
Update copyrights, add missing file-level documentation; fix perms.

10 years agoFixes related to parametric datatype printing.
Morgan Deters [Thu, 5 Dec 2013 17:54:40 +0000 (12:54 -0500)]
Fixes related to parametric datatype printing.

10 years agoFix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).
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).

10 years agoScript fixes; when determining authorship of source files, don't count copyright...
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.

10 years agoFix NEWS.
Morgan Deters [Thu, 5 Dec 2013 19:52:37 +0000 (14:52 -0500)]
Fix NEWS.

10 years agoNEWS reorganization.
Morgan Deters [Thu, 5 Dec 2013 19:36:14 +0000 (14:36 -0500)]
NEWS reorganization.

10 years agoRemove a regression for which the portfolio takes forever (see bug 542).
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).

10 years agoMinor cleanup.
Morgan Deters [Wed, 4 Dec 2013 21:45:23 +0000 (16:45 -0500)]
Minor cleanup.

10 years agoPartial kind branch merge, including new --rewrite-apply-to-const feature.
Morgan Deters [Wed, 4 Dec 2013 19:16:24 +0000 (14:16 -0500)]
Partial kind branch merge, including new --rewrite-apply-to-const feature.

10 years agoDon't put define-funs in model output; bug 411 testcase no longer relevant.
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.

10 years agoUpdated acknowledgments.
Morgan Deters [Wed, 4 Dec 2013 19:15:27 +0000 (14:15 -0500)]
Updated acknowledgments.

10 years agoMore Java bindings fixes
Morgan Deters [Wed, 4 Dec 2013 05:50:57 +0000 (00:50 -0500)]
More Java bindings fixes

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 4 Dec 2013 04:55:57 +0000 (22:55 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadds LB strategy
Tianyi Liang [Wed, 4 Dec 2013 04:53:02 +0000 (22:53 -0600)]
adds LB strategy

10 years agoadds LB strategy
Tianyi Liang [Wed, 4 Dec 2013 04:53:02 +0000 (22:53 -0600)]
adds LB strategy

10 years agoSome fixes for swig warnings.
Morgan Deters [Wed, 4 Dec 2013 01:49:39 +0000 (20:49 -0500)]
Some fixes for swig warnings.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 3 Dec 2013 23:05:58 +0000 (17:05 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoLast version for undelayed LB
Tianyi Liang [Tue, 3 Dec 2013 23:03:34 +0000 (17:03 -0600)]
Last version for undelayed LB

10 years agoLast version for undelayed LB
Tianyi Liang [Tue, 3 Dec 2013 23:03:34 +0000 (17:03 -0600)]
Last version for undelayed LB

10 years agoWork around a swig segfault issue when building on Mac OS
Morgan Deters [Tue, 3 Dec 2013 20:40:00 +0000 (15:40 -0500)]
Work around a swig segfault issue when building on  Mac OS

10 years agochange string news
Tianyi Liang [Tue, 3 Dec 2013 20:04:58 +0000 (14:04 -0600)]
change string news

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 3 Dec 2013 19:55:12 +0000 (13:55 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agostring fmf perfomance fix
Tianyi Liang [Tue, 3 Dec 2013 19:53:47 +0000 (13:53 -0600)]
string fmf perfomance fix

10 years agostring fmf changes
Tianyi Liang [Thu, 21 Nov 2013 18:36:44 +0000 (12:36 -0600)]
string fmf changes

10 years agostring fmf perfomance fix
Tianyi Liang [Tue, 3 Dec 2013 19:53:47 +0000 (13:53 -0600)]
string fmf perfomance fix

10 years agorm ChangeLog (use NEWS)
Kshitij Bansal [Tue, 3 Dec 2013 17:36:46 +0000 (12:36 -0500)]
rm ChangeLog (use NEWS)