feat(util/scoped_vec): add operator[]
feat(realpaver/rp_constraint): implement 'used' field
feat(dsolver/icp_solver): support int type
feat(dsolver/icp_solver): implement simple build_explanation

For the literals in m_stack, we only choose the ones used by ICP solver
and return to NRA solver as an explanation for the conflict (UNSAT)
fix(CMakeLists.txt): disable glog shared lib
fix(tools/basic/type.ml): use "%g" for printing numbers
fix(CMakeLists.txt): print EGLIBC message only in Linux
fix(CMakeLists.txt): clean up external dir structure; use NDEBUG for gflag
fix(util/git_sha1): add copyright, wrap with namespace
fix(main): cmd-line parsing

 - move cmd-line parsing from SMTConfig to main.
 - run gflags first, update argc and argv. Then call SMTConfig with the
   updated ones.
 - check whether a given file exists or not.

This closes dreal/dreal#39
fix(opensmt/smtsolvers/SMTConfig): fix nra_json_out_name
doc(*): update OCaml version dep (>=4.01.0)

[skip ci]
fix(CMakeLists.txt): use libunwind only for 64-bit linux
fix(tools/basic): separate each module out of big type file
fix(realpaver/rp_interval): fix log message
fix(realpaver/rp_lexer): support num literal: "[0-9]+E(+|-)?[0-9]+"
fix(CMakeLists, bin/dReach): use dReal instead of solver
feat(CMakeLists): add packaging via cpack
fix(CMakeLists): add static support for OS X
rp_lexer debug