Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Prettify SmtLib's selftest; fix bug

The now-deleted word example was perhaps being proved by earlier
versions of Z3, but Z3 4.4.0 and HOL both reckon the example is
false. (Depends on definition of signed modulus and -INT_MIN.)

Fix HolSmt’s selftest’s to cope with case-const arg-flip.

This is progress with github issue #97.

HOL4_{YICES,Z3}_EXECUTABLE evaluated at run-time (as opposed to compile time). Minor refactoring.

Made location of Yices and Z3 executables configurable. This allows to work
around issue #87.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Added SMT-LIB support for w ' i, by rewriting to (i >< i) w = 1w:word1.

Added SMT-LIB support for w2w (mapped to zero_extend) and sw2sw (mapped to
sign_extend).

Added warning messages to the Yices and SMT-LIB translations when type
operators or constants are treated as uninterpreted.

word_smod and bvsmod are mapped to each other again.

A few more tests about word_{div,mod} etc.

Added SMT-LIB support for word_{div,mod} and corresponding test cases.

Fixed a bug where nested let clauses defining the same variable were not
translated to SMT-LIB correctly. Corresponding self-test added. Thanks to
Bernard Blackham for reporting this issue.

The SMT-LIB translation now treats operations on polymorphic word types as
uninterpreted functions.

Fixed abstraction of higher-order goals into first-order formulas.

Minor cleanup.

Added Yices support for LSR_BV (via simplification to LSR).

Added SMT-LIB translation support for bit-vector rotations.

Added SmtLib support for word shift by number (via simplification).

Added (partial) support for shift operations that take two word arguments.

Added word_lsl_bv (<<~) to the Yices translation. Added corresponding self-tests.
Disabled word simplification for now, and added tracing output for the
simplified goal.

Major update, adding a translation from HOL to SMT-LIB 2 and enabling Z3 proof
checking again. (The latter still has some quirks, because Z3's proof
syntax is not fully SMT-LIB 2 compliant.)

Added Yices support for bit-vector extraction with bounds larger than the word
size. Thanks to Behzad for reporting this.

Major update, adding support for Z3 2.11 proofs (SMT-LIB 2 format).

Note that this breaks Z3 proof checking from HOL4 (for now), as no translation
from HOL4 into SMT-LIB 2 has been implemented yet.

Fixed the Yices translation of word_extract to adjust the size of the resulting
bit vector if necessary.

Added Yices support for sw2sw, typically mapping it to bv-sign-extend.

Added a test case (supplied by Yogesh Mahajan) that requires these features.

Better support for sets as predicates in HolSmtLib, replacing {x | P x} by P.

Towards support for sets as predicates.

Added Yices support for record types (field selection and update).

Added Yices support for data types (constructors and case constants).

Fixed a bug where def_axiom would fail on a provable term; added a self-test.

HolSmtLib now supports the Z3 2.0 proof format.

Simplified the interface to provide tactics only (use Tactical.TAC_PROOF or
similar to derive functions of type goal -> thm). Also simplified the
discharging of definitions in theorems derived by Z3.

Changed the interface to take a goal (i.e., a pair of assumption list and
conclusion) instead of a single term.

The same interface is provided by the SMT-LIB standard, which distinguishes
between assumptions and query formulas, and claims that "many SMT solvers can
process assumptions more efficiently if they are explicitly identified as
such." I don't know if that's true, but in any case, identifying them
explicitly is what we do now.

This is a major update, adding proof reconstruction for Z3 (and several smaller
improvements).

Fixed the Yices translation for signed vs. unsigned comparison operators on words.

Further operations on bit vectors added to the Yices translation.

Function w2w added to the Yices translation.

Further operations on bit vectors added to the Yices translation.

Word types and some word functions added to the Yices translation.

Support for solver CVC3 (via SMT-LIB input syntax) added.

Translation to SMT-LIB format (logic AUFLIA) implemented, solver YicesSMTOracle added. A few other (minor) changes.

Yices is now applied to beta-normal eta-long terms.

Support for tuple types, FST and SND added.

Major overhaul: the translation to Yices now uses a simple dictionary for most constants. Support for binders (quantifiers, lambda abstraction) added.

Yices support for div and mod added; minor other changes.

Unit tests added.