Merge branch '1.3.x'

mv prp to regress1

Merge branch '1.3.x'

fix bug 542

Initializing master for next version.

Initializing 1.3.x branch.

Cutting release 1.3.

disable substring in default mode

Fix NodeValue bitfields for 32-bit; fix comment.

Minor cleanup.

Update copyrights, add missing file-level documentation; fix perms.

Fixes related to parametric datatype printing.

Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).

Script fixes; when determining authorship of source files, don't count copyright-updating commits.

Fix NEWS.

NEWS reorganization.

Remove a regression for which the portfolio takes forever (see bug 542).

Minor cleanup.

Partial kind branch merge, including new --rewrite-apply-to-const feature.

Don't put define-funs in model output; bug 411 testcase no longer relevant.

Updated acknowledgments.

More Java bindings fixes

Merge branch 'master' of github.com:tiliang/CVC4

adds LB strategy

adds LB strategy

Some fixes for swig warnings.

Merge branch 'master' of github.com:tiliang/CVC4

Last version for undelayed LB

Last version for undelayed LB

Work around a swig segfault issue when building on  Mac OS

change string news

Merge branch 'master' of github.com:tiliang/CVC4

string fmf perfomance fix

string fmf changes

string fmf perfomance fix

rm ChangeLog (use NEWS)

SExpr pretty-printing for :all-options and :all-statistics.

Minor cleanup.

Add test case for (previously resolved) bug 528.

Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a subtype of (Pair Real Real).  Resolves bug #541.

fixed rewriter bug where postRewrite was not caching properly

Another fix to Java destruction order issues.  Thanks to Zheng Manchun for the report.

Update NEWS file.

Fix proofs build.

Fix portfolio compile error.

Ignore config/compile file, which newer autotools create

Fix for compile error when using gcc 4.7 with -std=gnu++11.  Thanks to Martin Brain for the patch!

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

Java bindings improvements for CASCADE, minor cleanup.

Add missing template instanatiation in Java bindings

Some versioning in advance of the 1.3 release.

Incremental is now on by default when using from API, off for command-line driver except in interactive mode.

Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter

Fix a segfault in the printer infrastructure when called from API and no language is set

Fix C++-to-Java exception translation.

Fix Java output stream adapter.

Merge branch 'master' of github.com:tiliang/CVC4

string fmf changes

Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.

Minor fix for swig bindings.

Merge remote-tracking branch 'CVC4root/master'

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.)

Array collectModelInfo fix for Andy

Merge branch 'master' of github.com:tiliang/CVC4

string fmf changes

string fmf changes

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.

Changing the number of bits allocated per field in node values.

Bug fix for previous commit

Add fair strategy for finite model finding multiple sorts --uf-ss-fair.

Minor fixes for Mac OS Mavericks

Allow empty record literals (fixing an oversight in previous work on empty tuples/records)

Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!

Datatype::getCardinality() caching

Add virtual destructors where missing

Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google for the report and patch!

Another build fix; the dust should be settled now.

Minor portfolio fixes for some platforms.

Some additional explanation for a common configure error.

lb change

add string progress measurements

Merge branch 'master' of github.com:tiliang/CVC4

add loop cache

add loop cache

Fix new-theory script for new, flattened build system.

Minor build system cleanup

length lemma is changed, var-split lemma is changed

Merge branch 'master' of https://github.com/CVC4/CVC4

Expanded usefulness of (set-info :cvc4-logic ...)

Some fixes to build system with dependency-tracking is off; should fix RPM/Debian builds.

Change exit status to be more consistent with other command-line tools: 0 success, nonzero error

Fix compat-java library naming on Mac OS; thanks to Zheng Manchun for reporting this issue

Merge branch 'master' of https://github.com/CVC4/CVC4

Fix "make distclean", which should fix some of the build issues from last night

Minor fixups to last commit

Flatten libcvc4 build structure; remove some #include interdependences

Fix "make distclean", which should fix some of the build issues from last night

Minor fixups to last commit

Flatten libcvc4 build structure; remove some #include interdependences

Adds the header file into makefile, solving building error; adds cache for derivative; disables loop detection when finite model finding is enabled.