Adding support for bool-to-bv

Squashed commit of the following:

commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Mar 6 00:16:16 2017 -0800

    Remove IFF case

commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date:   Mon Feb 20 12:37:06 2017 -0800

    proof support for bvcomp

commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 21:09:04 2017 -0800

    Added missing cases to operator<< for bv rewrite rules.

commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 11:43:51 2017 -0800

    Added rewrite rules for new bitvector kinds.

commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Feb 13 14:41:49 2017 -0800

    First draft of bool-to-bv pass.

Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.

Another minor fix for sets related to sharing + finite element types.

Fixes related to sets.

Minor cleanup and reorganization related to last commit.

Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

Minor fixes for relations, quantifiers dsplit.

Fixes for sets+rels check. Minor.

Minimization modes for fmf bound.

Generalize finite bound inference to unifiable variables in set membership literals.

Fix regexp cache issue in strings, add regression.

Fix non-idempotent rewrite in Array rewriter

This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.

Merge pull request #128 from 4tXJ7f/fix_lfsc_perf

[LFSC] Fix performance issues, more determinism

Minor fix in relations.

[LFSC] Fix performance issues, more determinism

For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.

Fix call to SExpr constructor for greater portability.

Merge pull request #130 from chadbrewbaker/master

Fixing memory leak

Do not rewrite explanations in strings.

Merge pull request #129 from timothy-king/regression-scrubber

Adding regression test scrubbing.

Merge pull request #131 from makaimann/fix_702

Proposed fix for bug 702

Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()

Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.

Merge pull request #127 from cristian-mattarei/issue_679

Bug 679 fix

revert

Quashing memory leak

Adding regression test scrubbing.

With reference to Bug 679, this commit integrates part of the patch proposed, and it fixes the correct float parsing of an std::istringstream.

The compilation issue in Bug 679 does not apply anymore with gcc6.3.1

quashing debug memory leak

Minor fix for sets.

Disabling a regression test that assumes CVC4 is configured with proofs on. Modifying the travis rules so there are instances with proofs disabled.

Fix for tff type declarations inTPTP parser, fixes bug 748.  Other minor changes.

Marking regression test files as non-executable.

Marking the proof signature files as non-executable.

Setting the executable bit for the newer run scripts in contrib.

Reverting two files encoding with DOS linebreaks back into using unix linebreaks.

Merge pull request #122 from 4tXJ7f/fix_lfsc_str

[LFSC] Minor fixes/improvements

Merge pull request #120 from 4tXJ7f/fix_f_pp_holes

Fix dependency tracing for fewerPreprocessingHoles

Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks

[LFSC] Fix memory leaks when creating CExprs

Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.

Eliminating a signed vs. unsigned comparison.

Changing getTearDownIncremental() to return the type of options::tearDownIncremental.

Adding a destructor to InstantiationNotify.

Adding a destructor to RepBoundExt.

Reordering sep and sets in Makefile.theories.

[LFSC] Minor fixes/improvements

- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions

[LFSC] Fix memory leaks when creating CExprs

In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).

Fix dependency tracing for fewerPreprocessingHoles

Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed.  Additionally, it fixes
a similar issue in the theory engine.

NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.

Merge pull request #119 from 4tXJ7f/smt_v2_5

Switch from SMT-LIB v2.0 to v2.5 for smt2 files

Switch from SMT-LIB v2.0 to v2.5 for smt2 files

As mentioned in bug 741, CVC4 was parsing `.smt2` files using the
SMT-LIB v2.0 standard by default. This commit switches to v2.5.

Made tear-down-incremental more like it used to be: when tear-down value
is 1, it does not automatically enable incremental mode.

Merge pull request #118 from 4tXJ7f/fix_emp

Fix split-find-unsat-w-emp test

Merge pull request #117 from 4tXJ7f/fix_order

Fix initialization order

Fix split-find-unsat-w-emp test

Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the
split-find-unsat-w-emp test, this commit fixes that.

Merge branch 'master' into fix_order

Merge pull request #116 from 4tXJ7f/fix_mult

Fix (inactive) `MultSlice` rewrite

Fixing a use after free bug in Polynomial::denominatorLCM.

Fix initialization order

This commit addresses the following warning:

```
warning: field 'd_negOne' will be initialized after field 'd_pivots'
[-Wreorder]
```

Fix (inactive) `MultSlice` rewrite

The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.

Enable remaining cardinality benchmarks

Add missing regression

Add sets regression, fixes bug 754.  Minor fix to regexp in strings.

Added cardinality to cvc language, fixes bug 753. Throw logic exception when using cardinality on sets with finite element type.

Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.

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

Turned off nonClausalSimplify when using fewerPreprocessingHoles.
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.

Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.

Fix nf exp tracking for non-linear string equalities, fixes bug 768.

Improve bounds for global heap in sep, refactor preprocessing. Minor improvement to sets.

Added "dump=raw-benchmark" option for dumping all user commands exactly as received.

Fix unit test for datatypes, add interface functions to datatypes.

Fix for bug 734

Cleaning up Statistics::copyFrom to avoid casts.

Initializing the d_pivots variable.

Merge pull request #95 from 4tXJ7f/fix_sierra_build

Revert "Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a…

Merge pull request #113 from 4tXJ7f/remove_extract_rule

Remove wrong `ExtractMultLeadingBit` rule

Bug fixes and refactoring of parametric datatypes, add some regressions.

Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.

Fix build on macOS Sierra

Before this fix, the build died with `ar: no archive members specified
when linking the empty libreplacements.la.` because macOS Sierra does
not require the replacements anymore. With this fix, `ffs.c` and
`strtok_r.c` are always getting compiled (even when they are empty) to
prevent the error. Also removed the unused
`CVC4_NEEDS_REPLACEMENT_FUNCTIONS` from `configure.ac` and added an
`#ifndef HAVE_FFS` to `ffs.c` for consistency with `strtok_r.c`.

Fix quantifiers dynamic splitting module for incremental mode, fixes bug 765 and 763.

Improvement and bug fix for str.indexof reduction, add regression. Other minor changes.

Remove wrong `ExtractMultLeadingBit` rule

The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.

Merge pull request #115 from 4tXJ7f/bug766

Fix parsing of BVROTR by CVC parser

Merge pull request #114 from 4tXJ7f/add_unit_test

Add unit test for `MultDistrib` rule

Fix parsing of BVROTR by CVC parser

This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.

Add unit test for `MultDistrib` rule

This unit test checks that the issue fixed by commit
c0c424283c12cfce2874ea92188487d91acecdf3 has been resolved.

Merge pull request #112 from 4tXJ7f/fix_mult_distrib

Fix `MultDistrib` rewrite rule

Fix smt2 and cvc printers for testers when output and input languages are different.

Merge pull request #111 from 4tXJ7f/fix_test_includes

Remove unused, libstdc++-exclusive include

Fix `MultDistrib` rewrite rule

The assertion in the `MultDistrib` rule would fail when doing:

```
Node expr = d_nm->mkNode(BITVECTOR_MULT, mkNode(BITVECTOR_SUB, x, y), z);
if (RewriteRule<MultDistrib>::applies(expr))
  RewriteRule<MultDistrib>::apply(expr);
```

When checking which side to distribute over, the code only checked for
`BITVECTOR_PLUS` instead of `BITVECTOR_PLUS` or `BITVECTOR_SUB` in
contrast to the other conditions in
`RewriteRule<MultDistrib>::applies()` and the assert.

NOTE: I was only able to reproduce this issue when testing the rewrite
rule in isolation. The rule `SubEliminate` generally seems to turn the
`BITVECTOR_SUB` node into a `BITVECTOR_PLUS` node before the rewriter
tries `MultDistrib`.

Remove unused, libstdc++-exclusive include

The file `ext/stdio_filebuf.h` does not seem to be available in libc++,
which made compilation of the unit tests for macOS unnecessarily
complicated given that it is not used anyway.

Refactoring related to track instantiation option.

Fix for unit test after changing default "all supported" logic name.

Removing some throw specifiers from OutputChannel. Fixes bug 716.

Merge pull request #110 from 4tXJ7f/fix_makefiles

Fix Makefiles in test

Modified a couple of regressoins to use ALL/QF_ALL instead of ALL_SUPPORTED/QF_ALL_SUPPORTED

Add support for set-logic ALL, fix compiler error in GCC 6.1

Fix Makefiles in test

With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.

Merge pull request #108 from timothy-king/smt2-parser-exception-leaks

Adding garbage collection for the Smt2 Parser for Commands when excep…

Merge pull request #109 from PaulMeng/master

relational solver code refactor and bug fixes

relational solver code refactor and bug fixes