Luận Văn Xây dựng hệ thống giải bài toán smt hiệu năng cao – phần máy trạm

Mục lục
Chương 1. Mở đầu 1
1.1. Giới thiệu . 1
1.2. Bài toán đặt ra 1
1.3. Cấu trúc nội dung tài liệu . 2
Chương 2. Kiến thức nền tảng 3
2.1. Giới thiệu SMT 3
2.2. Bộgiải SMT (SMT solver) 3
2.3. Thưviện SMT (SMT-LIB) 4
2.3.1. Cấu trúc cơbản của SMT-LIB . 4
2.3.2. Khuôn dạng của SMT-LIB . 5
Chương 3. Phân tích hệthống 12
3.1. Mô hình hệthống . 12
3.2. Mô hình ca sửdụng của hệthống 13
3.3. Mô hình hoạt động . 15
Chương 4. Phương hướng giải quyết vấn đề 17
4.1. Lựa chọn phương thức kết nối . 17
4.2. Lựa chọn ngôn ngữlập trình 17
4.3. Xác định dữliệu đầu vào, đầu ra của hệthống 17
Chương 5. Mô tảhệthống 19
5.1. Quy định cách thức giao tiếp với máy chủ 19
5.2. Phần máy khách . 20
5.2.1. Quy định giao tiếp với máy chủ . 20
5.2.2. Các lớp của hệthống máy khách 21
5.2.2.1. Lớp config . 21
5.2.2.2. Lớp Client: 21
5.2.2.3. Lớp NetSolver . 21
5.2.2.4. Lớp Bench_attribute 22
5.2.2.5. Lớp Formula 22
5.2.2.6. Lớp func_decl 23
5.2.2.7. Lớp pred_decl 24
5.2.2.8. Lớp Term . 24
5.2.2.9. Lớp annotation 24
5.2.2.10. Lớp varDecl 24
5.2.2.11. Lớp fvarDecl . 24
5.2.2.12. Lớp Arith_symb 25
5.2.2.13. Lớp Identifier 25
5.2.2.14. Lớp quant_var . 25
5.3. Phần máy trạm . 26
5.3.1. Cơchếlàm việc của máy trạm . 26
5.3.2. Quy định giao tiếp với máy chủ . 27
5.3.3. Hoạt động của hệthống máy trạm 28
5.3.4. Các lớp của hệthống máy trạm 30
5.3.4.1. Biểu đồlớp của hệthống . 30
5.3.4.2. Lớp config . 30
5.3.4.3. Lớp sessionID 30
5.3.4.4. Lớp Solver . 31
5.3.4.5. Lớp ReadThread 31
5.3.4.6. Lớp WriteThread . 34
5.4. Tổng kết . 34
Chương 6. Cài đặt và thửnghiệm . 36
6.1. Cài đặt 36
6.2. Bài toán thực nghiệm . 36
6.2.1. Xây dựng bài toán SMT dựa trên các hàm API 36
6.2.2. Thửnghiệm kết nối với máy chủvà toàn hệthống 37
Hướng phát triển tiếp theo của hệthống 40