Updates mostly related to satlink/tshell

TSHELL:
  - Extended tshell with optional output filters (fixes issue 119)
  - Fixed bug with tshell incorrectly handling commands that don't print a final newline

SATLINK:
  - Added basic satlink config-checking function
  - Added script for using Glucose with drup-trim (Marijn Heule's UNSAT proof checker)
  - Added output filter for SATLINK so that variable lines aren't printed
  - Added some documentation on available SAT solvers and drup-trim

VL:
  - Tweak how VL generates multipliers, to better match GL multiplication
  - Update centaur/regression/multiply.lisp to verify larger multipliers

MISC:
  - Fixed a couple of problems in define's untranslate stuff
  - Fixed a problem with :xdoc in strange guard-checking modes
  - Start of a Boolean Expression Diagram (bed) library (very preliminary)
  - Minor tweaks to centaur tutorial due to VL/Satlink changes

Update issue 123

This doesn't really address the greater problem of having ACL2 verify
SAT proofs, but at least gives a way to use an unverified checker to
check proofs from the solver, and improve the soundness story.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2351 303c5b2c-9740-0410-b014-fd8f9db7be32
gl: fix a non-bug, vl: add a distinguishing attribute to temp wires introduced by xf-expr-split

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2352 303c5b2c-9740-0410-b014-fd8f9db7be32