#solver Hỗ trợ giải hệ ràng buộc
#Yêu cầu JDK 8, jeval (http://jeval.sourceforge.net/), Z3 (32 bit/64 bit tùy vào cấu hình máy tính)
Sản phẩm mới được test trên hệ điều hành win 7 (chưa test trên ubuntu, MAC)
#Cách dùng B1. Vào SolutionGeneration trong solver.main, nhập danh sách tên biến (test cases) và hệ ràng buộc (constraints)
B2. Cấu hình thông số đường dẫn Z3Configuration.Smt_Lib_path_file và Z3Configuration.Smt_Lib_path_lib
B3. Enjoy. Đầu ra nếu có nghiệm sẽ trình bày nghiệm trong Console và ngược lại.