Simplified the core logic of the under-constrained analyzer
Refactored the I/O related functions to a new file in an attempt to further modularize the code. Specifically, we no longer create a new solver, but instead, utilize the stack-like functionality of Z3 that allows us to store and pop the constraints.
Made the code more readable by utilizing enums and structs (e.g. AnalyzerInput, AnalyzerOutputStatus)
AnalyzerInput,AnalyzerOutputStatus)