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.

Stopping non-linear terms from entering the dio solver. Fixes bug 547.

URL update

Fix for quote-escaping in smt2 printer

enable search for html doc

gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)

Switch license default back to BSD, and add --best and --enable-gpl options.

Cache apt packages on Travis.

Fix LogicInfo parsing for string logics

Update copyright year.

Fix for ANTLR warning.

Better automatic handling of output language setting.

Better get-value parse error message for common user error.

Minor code cleanup.

cln now default w.r.t. build ID string

Fix to interactive mode determination.

Fix option specification.

Fix an autoconf issue with CLN in some configurations; also clarification re: license issues

[skip ci]

Fix configure handling for CLN (should fix win32 nightly builds)

Add missing regression-results directory.

configure --with-portfolio disables CLN.

some config changes: new --bsd option, readline gives warning, default build is now production.

Send Travis-CI emails to everyone

Fix for bug 544.

Another fix for clang.

Fix stack size on in-tree regressions.

cleanup

Fix link error when using clang.

Fix to Travis-CI config.

Travis-CI configuration.

Some minor cleanup.

Update NEWS.

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

mv prp to regress1

fix bug 542

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