Updating: improving FALCON/falcon_cnfize
Updating: miscellaneous
Changed s2exp normilization to ignore s2var when exporting constraints. The reasoning behind this is that when we replace s2var's with expressions they represent, the SMT solver is unable to understand equality between two static variables.
Adding in Z3 interface from Anairiats
Used ATS2 conventions for function signatures
Added a small solving file that builds off of constraint and parsing
Added a generic solver component that any SMT solver may be used internally.
Have a stand alone file working
Added a typechecking shell that wraps functions defined by individual SMT solvers.
Adding the s2cst map into the typechecker.
Adding the s2cst map
Added in the solver agnostic interface for SMT.
Converting more of the SMT code to ATS2
Added an implementation for linmap_listize for linmap_avltree
Verified the listize function compiles properly now.
Worked in the new naming conventions for dynload files.
Added more of the constraint solver into ATS2
Simplified the way termination constraints are represented in JSON to a normalized form.
Worked in the h3ypo code.
Added Z3's implementation of the SMT interface