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: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
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
Morgan Deters [Tue, 26 Nov 2013 20:25:59 +0000 (15:25 -0500)]
Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.
Morgan Deters [Tue, 26 Nov 2013 20:05:52 +0000 (15:05 -0500)]
Minor fix for swig bindings.
Tim King [Mon, 25 Nov 2013 23:41:06 +0000 (18:41 -0500)]
Merge remote-tracking branch 'CVC4root/master'
Tim King [Mon, 25 Nov 2013 23:36:06 +0000 (18:36 -0500)]
Substantial Changes:
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
Clark Barrett [Mon, 25 Nov 2013 23:21:40 +0000 (15:21 -0800)]
Array collectModelInfo fix for Andy
Tianyi Liang [Thu, 21 Nov 2013 18:39:36 +0000 (12: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
Tianyi Liang [Thu, 21 Nov 2013 18:36:44 +0000 (12:36 -0600)]
string fmf changes
Tim King [Thu, 14 Nov 2013 16:56:34 +0000 (11:56 -0500)]
Adding the changes needed to delete rewriter attributes. This includes being able to list attributes. Additionally, added debugging hooks to node manager and attribute manager.
Tim King [Wed, 20 Nov 2013 01:57:15 +0000 (20:57 -0500)]
Changing the number of bits allocated per field in node values.
Andrew Reynolds [Tue, 19 Nov 2013 23:09:19 +0000 (17:09 -0600)]
Bug fix for previous commit
Andrew Reynolds [Tue, 19 Nov 2013 22:40:23 +0000 (16:40 -0600)]
Add fair strategy for finite model finding multiple sorts --uf-ss-fair.
Morgan Deters [Thu, 14 Nov 2013 14:30:25 +0000 (09:30 -0500)]
Minor fixes for Mac OS Mavericks
Morgan Deters [Thu, 14 Nov 2013 14:33:34 +0000 (09:33 -0500)]
Allow empty record literals (fixing an oversight in previous work on empty tuples/records)
Morgan Deters [Thu, 14 Nov 2013 02:20:11 +0000 (21:20 -0500)]
Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!
Morgan Deters [Thu, 14 Nov 2013 02:03:16 +0000 (21:03 -0500)]
Datatype::getCardinality() caching
Morgan Deters [Wed, 13 Nov 2013 23:20:17 +0000 (18:20 -0500)]
Add virtual destructors where missing
Morgan Deters [Wed, 13 Nov 2013 23:10:06 +0000 (18:10 -0500)]
Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google for the report and patch!
Morgan Deters [Wed, 13 Nov 2013 17:07:36 +0000 (12:07 -0500)]
Another build fix; the dust should be settled now.
Morgan Deters [Tue, 12 Nov 2013 23:13:17 +0000 (18:13 -0500)]
Minor portfolio fixes for some platforms.
Morgan Deters [Tue, 12 Nov 2013 23:12:11 +0000 (18:12 -0500)]
Some additional explanation for a common configure error.
Tianyi Liang [Tue, 12 Nov 2013 22:46:01 +0000 (16:46 -0600)]
lb change
Tianyi Liang [Tue, 12 Nov 2013 21:49:39 +0000 (15:49 -0600)]
add string progress measurements
Tianyi Liang [Tue, 12 Nov 2013 19:39:58 +0000 (13:39 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 12 Nov 2013 19:33:15 +0000 (13:33 -0600)]
add loop cache
Tianyi Liang [Tue, 12 Nov 2013 19:33:15 +0000 (13:33 -0600)]
add loop cache
Morgan Deters [Tue, 12 Nov 2013 15:10:45 +0000 (10:10 -0500)]
Fix new-theory script for new, flattened build system.
Morgan Deters [Tue, 12 Nov 2013 15:08:39 +0000 (10:08 -0500)]
Minor build system cleanup
Tianyi Liang [Tue, 12 Nov 2013 01:45:07 +0000 (19:45 -0600)]
length lemma is changed, var-split lemma is changed
Tianyi Liang [Mon, 11 Nov 2013 17:32:45 +0000 (11:32 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4
Morgan Deters [Mon, 11 Nov 2013 16:51:07 +0000 (11:51 -0500)]
Expanded usefulness of (set-info :cvc4-logic ...)