add Symbol
add SymbolicExec
add SymbolicExec.main which outputs z3-smt
add symbol handling
refactor: toExpr -> toSMTExpr
add Lua->SMT operator conversion