Tim King [Tue, 1 Apr 2014 20:54:36 +0000 (16:54 -0400)]
Fixing bug 552. There was a bug when integers are made using a string with a lot of leading 0s on old versions of CLN.
Morgan Deters [Tue, 25 Mar 2014 23:53:10 +0000 (19:53 -0400)]
Win32 build script fixes (to allow portfolio builds).
Morgan Deters [Wed, 26 Mar 2014 22:05:02 +0000 (18:05 -0400)]
Fix an off-the-end string pointer bug (showed up only in some Win32 builds).
Tim King [Wed, 26 Mar 2014 20:56:13 +0000 (16:56 -0400)]
Fixes an idempotency issue for non-linear multiplication with integer and real variables.
Morgan Deters [Tue, 11 Mar 2014 22:50:51 +0000 (18:50 -0400)]
Fix for random-seed option.
Morgan Deters [Tue, 11 Mar 2014 22:47:28 +0000 (18:47 -0400)]
Fix for portfolio.
Morgan Deters [Tue, 11 Mar 2014 19:07:38 +0000 (15:07 -0400)]
Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.
Morgan Deters [Fri, 21 Feb 2014 22:15:43 +0000 (17:15 -0500)]
No diamond-breaking under quantifiers (resolves bug #550).
Morgan Deters [Fri, 21 Feb 2014 19:45:52 +0000 (14:45 -0500)]
Fix two variants of Node::substitute().
Node::substitute() is overloaded. One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted). The others were
ignoring anything in function position. Fixed. Thanks to Wei Wang for
pointing this out.
Tim King [Wed, 19 Feb 2014 20:50:07 +0000 (15:50 -0500)]
Stopping non-linear terms from entering the dio solver. Fixes bug 547.
Morgan Deters [Mon, 27 Jan 2014 23:04:04 +0000 (18:04 -0500)]
URL update
Morgan Deters [Sat, 18 Jan 2014 03:59:39 +0000 (22:59 -0500)]
Fix for quote-escaping in smt2 printer
Kshitij Bansal [Fri, 17 Jan 2014 14:11:58 +0000 (09:11 -0500)]
enable search for html doc
Morgan Deters [Thu, 9 Jan 2014 21:48:21 +0000 (16:48 -0500)]
gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)
Morgan Deters [Wed, 8 Jan 2014 20:27:26 +0000 (15:27 -0500)]
Switch license default back to BSD, and add --best and --enable-gpl options.
Morgan Deters [Wed, 18 Dec 2013 02:13:12 +0000 (21:13 -0500)]
Cache apt packages on Travis.
Morgan Deters [Wed, 8 Jan 2014 16:18:02 +0000 (11:18 -0500)]
Fix LogicInfo parsing for string logics
Morgan Deters [Thu, 2 Jan 2014 19:13:08 +0000 (14:13 -0500)]
Update copyright year.
Morgan Deters [Fri, 27 Dec 2013 17:21:20 +0000 (12:21 -0500)]
Fix for ANTLR warning.
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 [Mon, 23 Dec 2013 18:45:33 +0000 (13:45 -0500)]
cln now default w.r.t. build ID string
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.
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:50 +0000 (11:47 -0500)]
Fix configure handling for CLN (should fix win32 nightly builds)
Morgan Deters [Wed, 18 Dec 2013 16:09:41 +0000 (11:09 -0500)]
Add missing regression-results directory.
Morgan Deters [Tue, 17 Dec 2013 23:56:19 +0000 (18:56 -0500)]
configure --with-portfolio disables CLN.
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 [Mon, 16 Dec 2013 19:34:38 +0000 (14:34 -0500)]
Send Travis-CI emails to everyone
Morgan Deters [Mon, 16 Dec 2013 12:30:06 +0000 (07:30 -0500)]
Fix for bug 544.
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: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: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 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: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: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
Tianyi Liang [Tue, 3 Dec 2013 20:04:58 +0000 (14:04 -0600)]
change string news
Tianyi Liang [Tue, 3 Dec 2013 19:55:12 +0000 (13:55 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 3 Dec 2013 19:53:47 +0000 (13:53 -0600)]
string fmf perfomance fix
Tianyi Liang [Thu, 21 Nov 2013 18:36:44 +0000 (12:36 -0600)]
string fmf changes
Tianyi Liang [Tue, 3 Dec 2013 19:53:47 +0000 (13:53 -0600)]
string fmf perfomance fix
Kshitij Bansal [Tue, 3 Dec 2013 17:36:46 +0000 (12:36 -0500)]
rm ChangeLog (use NEWS)
Morgan Deters [Tue, 30 Jul 2013 23:06:23 +0000 (19:06 -0400)]
SExpr pretty-printing for :all-options and :all-statistics.
Morgan Deters [Tue, 3 Dec 2013 00:32:59 +0000 (19:32 -0500)]
Minor cleanup.
Morgan Deters [Tue, 3 Dec 2013 00:32:44 +0000 (19:32 -0500)]
Add test case for (previously resolved) bug 528.
Morgan Deters [Tue, 3 Dec 2013 00:32:14 +0000 (19:32 -0500)]
Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real). Resolves bug #541.
lianah [Tue, 3 Dec 2013 00:41:56 +0000 (19:41 -0500)]
fixed rewriter bug where postRewrite was not caching properly
Morgan Deters [Mon, 2 Dec 2013 22:54:32 +0000 (17:54 -0500)]
Another fix to Java destruction order issues. Thanks to Zheng Manchun for the report.
Morgan Deters [Thu, 26 Sep 2013 13:32:20 +0000 (09:32 -0400)]
Update NEWS file.
Morgan Deters [Fri, 29 Nov 2013 16:32:29 +0000 (11:32 -0500)]
Fix proofs build.
Morgan Deters [Fri, 29 Nov 2013 16:06:44 +0000 (11:06 -0500)]
Fix portfolio compile error.
Morgan Deters [Wed, 27 Nov 2013 23:28:42 +0000 (18:28 -0500)]
Ignore config/compile file, which newer autotools create
Morgan Deters [Wed, 27 Nov 2013 23:08:15 +0000 (18:08 -0500)]
Fix for compile error when using gcc 4.7 with -std=gnu++11. Thanks to Martin Brain for the patch!
Morgan Deters [Wed, 3 Jul 2013 21:13:31 +0000 (17:13 -0400)]
General pre-release cleanup commit
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
Morgan Deters [Wed, 27 Nov 2013 22:37:30 +0000 (17:37 -0500)]
Java bindings improvements for CASCADE, minor cleanup.
Morgan Deters [Wed, 27 Nov 2013 20:35:03 +0000 (15:35 -0500)]
Add missing template instanatiation in Java bindings
Morgan Deters [Wed, 27 Nov 2013 16:23:01 +0000 (11:23 -0500)]
Some versioning in advance of the 1.3 release.
Morgan Deters [Wed, 27 Nov 2013 16:12:11 +0000 (11:12 -0500)]
Incremental is now on by default when using from API, off for command-line driver except in interactive mode.
Andrew Reynolds [Wed, 27 Nov 2013 01:02:21 +0000 (19:02 -0600)]
Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter
Morgan Deters [Tue, 26 Nov 2013 21:37:06 +0000 (16:37 -0500)]
Fix a segfault in the printer infrastructure when called from API and no language is set
Morgan Deters [Tue, 26 Nov 2013 21:36:52 +0000 (16:36 -0500)]
Fix C++-to-Java exception translation.
Morgan Deters [Tue, 26 Nov 2013 21:36:29 +0000 (16:36 -0500)]
Fix Java output stream adapter.
Tianyi Liang [Tue, 26 Nov 2013 20:39:13 +0000 (14:39 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 21 Nov 2013 18:36:44 +0000 (12:36 -0600)]
string fmf changes