Add test for shared scalar variable in single thread
Use SMT function to encode read-from schedules

A read event is affected by at most one write event.
Add TagAtomSet helper

This helper allows us to decompose a Tag into its constituent parts.
Use "unsigned int" type for tag atoms

This facilities interfacing with Z3.
Use "unsigned int" for event identifiers

This facilitates interfacing with Z3.
Fix incorrect numerical type for thread identifiers
Use C++11 for-each loop to iterate over body events
Consistently name axiom encoding functions
Document per-thread encoding function and hide internals