ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Hoàng Thế Tùng 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
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY
Ngành: Công nghệ phần mềm Cán bộ hướng dẫn: TS. Trương Anh HoàngCán bộ đồng hướng dẫn:
TS. Phạm Ngọc Hùng
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
2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Tóm tắt nội dung
Vấn đề giải quyết các bài toán Satisfiability Modulo Theories (SMT) hiện nay
đang được nghiên cứu và phát triển ở nhiều nơi trên thế giới. Cho đến ngày nay, nhiều
trường đại học, tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán
SMT (hay còn gọi là SMT solver). Ví dụ như Z3 của Mcrosoft, yices của SRI, CVC3
của một số trường đại học danh tiếng của Mỹ. hay boolector, openSMT của một số
trường đại học danh tiếng khác… Tuy nhiên, mỗi solver có một lợi thế ưu điểm riêng
đối với các dạng khác nhau của bài toán SMT. Vậy vấn đề đặt ra là làm sao để tận
dụng được hết các ưu điểm đó cho từng bài toán.
Để giải quyết vấn đề ấy, nhóm nghiên cứu đã nghiên cứu và xây dựng một hệ
thống giải quyết bài toán SMT trực tuyến, kết hợp nhiều bộ giải khác nhau để đưa ra
được lời giải tối ưu cho từng bài toán SMT.
Trong khuôn khổ khóa luận tốt nghiệp này của cá nhân tôi, tôi đã xây dựng hai
hệ thống con của hệ thống đã nêu trên là hệ thống trên máy khách (users) và trên máy
trạm (sử dụng để gọi các Solver). Hệ thống trên máy khách sẽ đảm nhiệm việc cung
cấp một giao diện lập trình ứng dụng (Application Programming Interface hay API) để
người dùng sử dụng có thể xây dựng bài toán SMT theo chuẩn thư viện SMT (SMT-
LIB) và sau đó là gửi bài toán đến máy chủ (server). Hệ thống trên máy trạm sẽ tiếp
nhận bài toán từ máy chủ và gọi các bộ giải để giải quyết bài toán đó và gửi về máy
chủ kết quả.
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
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.
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 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
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 40Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm
2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Danh sách các bảng trong tài liệu
Từ viết tắt Từ chuẩn Diễn giải
SMT Satisfiability Modulo Theories
Các lý thuyết module về
tính thỏa được
SMT-LIB
Satisfiability Modulo Theories -
Liblary
Thư viện các lý thuyết
module về tính thỏa được
API
Application Programming
Interface
Giao diện lập trình ứng
dụng 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
2010 Trang 1
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Chương 1. Mở đầu
1.1. Giới thiệu
Hiện nay, cùng với sự phát triển bùng nổ của hầu hết các ngành khoa học,
ngành khoa học máy tính cũng có những tiến bộ to lớn. Song song với đó, nhu cần
nghiên cứu về việc giải hoặc đưa ra tính khả thi của một biểu thức logic ngày càng
được quan tâm và phát triển. Bởi lẽ, rất nhiều các ứng dụng hay những sự tính toán
cho các bộ giải và nhận về kết quả trả về tối ưu nhất về mặt thời gian. Ngoài ra để tiện
cho việc sử dụng và phát triển hệ thống, cần có một thư viện các hàm nhúng hỗ trợ
người sử dụng xây dựng các vấn đề SMT.
1.3. Cấu trúc nội dung tài liệu
Tài liệu này nhằm giới thiệu về bài toán SMT và mô tả hệ thống giải quyết bài
toán đó trực tuyến. Chương mở đầu của tài liệu giới thiệu qua về bài toán SMT và bài
toán đặt ra cho việc xây dựng hệ thống giải quyết bài toán SMT đó.
Chương thứ hai của tài liệu đề cập tới một số kiến thức về SMT và cấu trúc,
khuôn dạng của bài toán SMT được xây dựng theo chuẩn SMT-LIB. Chương này được
coi là kiến thức nền tảng để xây dựng hệ thống giải quyết bài toán SMT hiệu năng cao.
Những kiến thức trong chương này sẽ được sử dụng để xây dựng các hàm API cho hệ
thống máy khách và một số thành phần của hệ thống máy trạm.
Chương ba và chương bốn là phần phân tích và hướng giải quyết vấn đề xây
dựng hệ thống giải bài toán SMT hiệu năng cao. Chương ba sẽ tập trung hơn vào vấn
đề phân tích, đưa ra một cái nhìn tổng quan về hệ thống và quy trình hệ thống sẽ hoạt
động. Chương bốn sẽ là một số lựa chọn giải pháp để giải quyết một số vấn đề khi xây
dựng hệ thống.
Hệ thống giải bài toán SMT hiệu năng cao phần máy trạm và máy khách sẽ được
mô tả chi tiết trong chương năm. Ở chương này, hệ thống các hàm API trên máy khách
sẽ được mô tả rất chi tiết và có thể coi là tài liệu hướng dẫn cho người dùng sử dụng
các hàm API này.
Chương sáu sẽ đưa ra phần thực nghiệm và đánh giá kết quả của hệ thống. Trong
chương này, kết quả của một số thực nghiệm hệ thống sẽ được đưa ra nhằm đưa ra một
số ưu điểm mà hệ thống có được.
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
2010
2010 Trang 4
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
đặt ra ở đây là kết quả của bộ giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều
các bộ giải như Absolver, Boolector, CVC3, OpenSMT, Yices, Z3…
Do yêu cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán
SMT đó có thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức năng này. Ngoài
ra hệ thống sử dụng đầu vào theo chuẩn của SMT-Lib và ngắt thời gian giải một bài
toán (trong trường hợp bài toán cần thời gian giải quá lớn), do đó, bộ giải cần phải có
hỗ trợ những chức năng này khi hoạt động. Từ những yêu cầu đó, nhóm nghiên cứu và
phát triển hệ thống đã quyết định sử dụng song song hai bộ giải là Yices của SRI
International và Z3 của Microsoft. Hai bộ giải này tuy có cấu trúc khác nhau nhưng
cùng được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-Loveland) [5]. Việc
tìm hiểu, phân tích cấu trúc cũng như thuật toán của hai bộ giải này sẽ không được đề
cập cụ thể ở đây.
2.3. Thư viện SMT (SMT-LIB)
Đề giải quyết các vấn đề SMT, việc nghiên cứu và đưa ra một chuẩn đầu vào là
rất cần thiết. Thông thường, mỗi bộ giải SMT đều có một quy định riêng cho chuẩn
đầu vào của mình, tuy nhiên như vậy sẽ thực sự khó khăn đối với việc thực thi một đầu
vào bởi các bộ giải khác nhau. Vì vậy, việc nghiên cứu và đưa ra một chuẩn đầu vào
thống nhất là rất cần thiết.
Khoảng tháng tư năm 2004, Silvio Rainise và Cesare Tinelli đã đưa ra chuẩn về
SMT-LIB đầu tiên [6]. Thời gian sau đó, họ liên tục cải tiến chuẩn đầu vào, bổ sung
những quy định chuẩn, thuyết mới. Cho đến nay, hai tác giả này đã và đang xây dựng
chuẩn SMT-LIB đã có phiên bản 2.0, tuy nhiên việc xây dựng đầu vào dựa trên chuẩn
mới này chưa được phổ biến. Hầu hết các bộ giải cũng như đầu vào cho các vấn đề
LIB Σ là một bộ dữ liệu bao gồm:
- Một tập không rỗng
∑
⊆
ௌ
ܲ các ký hiệu phân cấp (sort symbol), một tập
hợp ký hiệu hàm (function symbol)
∑
⊆
ி
ܨ và tập hợp các ký hiệu vị từ
(predicate symbol)
∑
⊆
ܲ;
- Một toàn ánh (total mapping) từ các biến (term variables) X tới Σ
S
;
- Một quan hệ toàn phương (total relation) từ Σ
F
đến (Σ
S
)
+
, một chuỗi các
thành phần của Σ
S
, không bao giờ có một cặp định dạng (f,s
1
- Không tồn tại khai báo định dạng f,s
1
…s
n
s và f,s
1
…s
n
s’ cho cùng một ký
tự hàm f mà s và s’ khác nhau;
- Tất cả các rút gọn trong khai báo ký tự hàm, vị từ được liệt kê trong khai
báo thuộc tính “sort”;
- Định nghĩa của lý thuyết được quy định trong thuộc tính “definition” và
chỉ liên quan đến các khai báo ký tự phân cấp, ký tự hàm và ký tự vị từ;
- Công thức trong thuộc tính “axiom” được xây dựng trên các khái báo ký
tự trong các thuộc tính “sort”, “funs”, “pred”.
Định nghĩa 4 (Khai báo Logic): Chỉ có một luật Logic được khai báo trong một
bài toán SMT và phải được thỏa mãn các giới hạn sau:
- Chúng bao gồm các khai báo thuộc tính “theory” và “language”;
- Chúng chứa ít nhất một khai báo đối với một thuộc tính;
- Giá trị của thuộc tính “theory” phải trùng với tên của thuyết T cho vài khai
báo của D
T
trong SMT-LIB.
Định nghĩa 5 (Khai báo về chuẩn): luật khai báo chuẩn phải thỏa mãn những
giới hạn sau:
- Chúng chứa chính xác một khai báo của thuộc tính “logic”, “formula” và
“status”;
- Giá trị của thuộc tính “logic” phải trùng khớp với tên của logic L cho vài
khai báo D
và g
ạ
ch dư
ớ
i , b
ắ
t đ
ầ
u b
ở
i ký t
ự
(2)
< user_value_content> ::= Bất kỳ chuỗ ký tự có thể in ra được
(3)
< user_value> ::= {< user_value_content>}
(4)
<numeral> ::= 0 | chuỗi không rỗng các chữ số bắt đầu khác 0
(5)
<rational> ::= <numeral>.0*<numeral>
(6)
<
indexed_
identifier
::=
<identifier> | <arith_symb>
(13)
<pred_symb> ::= <identifier> | <arith_symb> | distinct
(14)
<sort_symb> ::= <identifier>
(15)
<annotation> ::= <attribute> | <attribute> < user value>
(16)
<base_term> ::= <var> | <numeral> | <rational> | <identifier>
(17)
<an_term> ::= <base_term> | (<base_term> <annotation>
+
)
| (<funs_symb> <an_term>
+
<annotation>*)
| (ite <an_formula> <an_terrm> <an_term>
<annotation>*)
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
2010
<quant_var> ::= ( <var> <sort_symb>)
(6)
<an_formula> ::= <an_atom>
| ( <connective> <an formula>
+
<annotation>* )
| (<quant_symb> <quant_var>
+
<an_formula>
<annotation>* )
| (let (<var> <an_term>) <an_formula> <annotation>*
)
| ( flet ( <fvar> <an_formula> ) <an_formula>
<annotation>* )
Bảng 3: Luật sinh một thuyết
(1)
<string_content> ::= chuỗi liên tiếp các ký tự
(2)
<string> ::= “<string_content>”
(3)
<fun_symb_decl> ::= (<func_symb> <sort_symb>
+
<annotation>*)
| (<numeral> <sort_symb> <annotation>*)
| (<rational> <sort_sumb> <annotation>*)
<logic_attribute> ::= : theory <theory_name>
| :language <string>
| :extensions <string>
| :notes <string>
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
2010 Trang 9
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
| <annotation>
(3)
<logic> ::= (logic <logic_name> <logic_attribute>
+
)
Bảng 5 Luật sinh một chuẩn
(1)
<status> ::= sat | unsat | unknown
(2)
<bench_name> ::= <identifier>
(3)
<bench_attribute> ::= :logic <logic_name>
| :assumption <an_formula>
dữ liệu bit vector
Empty
Thuyết trống với ký hiệu rỗng
Ints
Số nguyên
Int_Arrays
Mảng số nguyên
Int_ArraysEx
Mảng giá trị được đánh thứ tự số nguyên với tiền
đề mở rộng
Int_Int_Real_Array_ArraysEx
Mảng của mảng các số nguyên và số thực với tiền
đề mở rộng
Reals
Số thực
Reals_Ints
Số nguyên và số thực
Nội dung cụ thể của từng lý thuyết xin được không đề cập đến ở đây để tránh
việc trình bày lan man không cần thiết.
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
2010 Trang 10
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng
Các logic cơ bản được áp dụng trong định dạng của SMT-LIB:
Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2
QF_LRA
Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số thực
QF_NIA
Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số
nguyên với ít nhất một đa thức không tuyến tính
QF_RDL
Logic khác của số thực, ví dụ bất đẳng thức x – y < b với x,y là
số thực và b là một hằng số hữu tỷ
QF_UF
Công thức vô lượng hóa (Unquantified formulas) xây dựng
trên ký hiệu của ký tự phân cấp, ký tự hàm, ký tự vị từ không
QF_UFIDL
Logic khác trên số nguyên nhưng với những ký tự phân cấp, ký
tự hàm, ký tự vị từ không được giải thích
QF_UFBV
Công thức vô lượng hóa trên kiểu bitvectors với ký tự hàm và
ký tự vị từ.
QF_UFLIA
Phép tính số nguyên vô lượng hóa tuyến tính với ký tự phân
cấp, ký tự hàm và ký tự vị từ
QF_UFLRA
Phép tính số thực vô lượng hóa tuyến tính với ký tự phân cấp,
ký tự hàm và ký tự vị từ
QF_UFNRA
Phép tính số thực vô lượng hóa không tuyến tính với ký tự
phân cấp, ký tự hàm và ký tự vị từ
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
2010
xây dựng hệ thống giải quyết vấn đề SMT trực tuyến qua mạng. Hệ thống sẽ được chia
ra làm ba phần rõ rệt là phần máy khách gửi yêu cầu giải quyết vấn đề, phần máy chủ
xử lý và phân phối các vấn đề nhận được, và phần máy trạm giải quyết vấn đề được
yêu cầu. Mô hình hệ thống được xây dựng như sau:
Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao.
Việc xây dựng phát triển hệ thống giải quyết vấn đề SMT trực tuyến sẽ đáp ứng
được yêu cầu về hiệu năng xử lý đầu vào. Hệ thống sẽ tiếp nhận một lúc nhiều 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
2010 Trang 13
Sinh viên: Hoàng Th
ế
n. V
ớ
i m
ỗ
i v
ấ
n
đề
nh
ậ
n
đượ
c, h
ệ
th
ố
ng s
ẽ
phân ph
ố
i
cho t
ấ
t c
ả
các b
ộ
gi
ả
cho phía yêu c
ầ
u.
Đố
i v
ớ
i nh
ữ
ng b
ộ
gi
ả
i
đư
a ra k
ế
t qu
ả
sau s
ẽ
nh
ậ
n
đượ
c tín hi
ệ
u d
ừ
ng
ầ
u c
ầ
n x
ử
lý là
đ
i
ề
u t
ấ
t y
ế
u, vì v
ậ
y, h
ệ
th
ố
ng máy ch
ủ
v
ừ
a
đả
m nh
ậ
n vi
ệ
c
ậ
y. V
ề
phía máy tr
ạ
m, m
ỗ
i máy tr
ạ
m s
ẽ
luôn nh
ậ
n và x
ử
lý nhi
ề
u các
v
ấ
n
đề
m
ộ
t lúc và ph
ả
i tr
ả
v
ề
ầ
n ph
ả
i có m
ộ
t th
ư
vi
ệ
c các hàm nhúng API
để
ng
ườ
i s
ử
d
ụ
ng tr
ự
c ti
ế
p xây d
ự
ng v
ấ
n
đề
SMT và g
ử
đượ
c coi nh
ư
là m
ộ
t tác nhân trung gian giúp duy trì t
ươ
ng tác gi
ữ
a chúng v
ớ
i nhau.
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
2010
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
GVHD:
TS. Trương Anh Hoàng
GVĐHD:
TS. Ph
ạ
m Ng
ọ
c Hùng
Hình 3.3: Mô hình hoạt động của hệ thống
Từ biểu đồ hoạt động của hệ thống, ta có thể xác định được các công việc tuần
tự của hệ thống và cách làm việc của hệ thống như sau:
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
2010 Trang 16
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
Đ
H Công ngh
ủ
và xây d
ự
ng bài
toán SMT. Bài toán SMT có th
ể
đ
ã
đượ
c mô t
ả
b
ằ
ng t
ệ
p tin hay
đượ
c xây d
ự
ng b
ằ
ng
ch
ươ
ng trình v
ớ
i vi
ệ
c s
i g
ử
i thông tin
v
ề
th
ờ
i gian gi
ớ
i h
ạ
n th
ự
c hi
ệ
n gi
ả
i bài toán và ch
ờ
đợ
i k
ế
t qu
ả
tr
ả
v
ề
t
ử
i t
ừ
máy khách, máy ch
ủ
s
ẽ
phân ph
ố
i các
bài toán
đ
ó cho các máy tr
ạ
m có b
ộ
gi
ả
i các bài toán SMT
đ
ang k
ế
t n
ố
i
đế
n máy ch
ủ
và
u vi
ệ
c th
ự
c hi
ệ
n gi
ả
i bài toán,
khi
đ
ó giá tr
ị
v
ề
tr
ễ
th
ờ
i gian cho m
ỗ
i bài toán s
ẽ
đượ
c s
ử
d
ụ
ng. Sau khi h
có hai tr
ườ
ng h
ợ
p x
ả
y
ra ti
ế
p sau
đ
ó. Tr
ườ
ng h
ợ
p m
ộ
t là máy tr
ạ
m
đ
ó s
ẽ
gi
ả
i ra k
ế
t qu
ả
nhanh nh
ã
có máy tr
ạ
m khác g
ử
i
đượ
c k
ế
t qu
ả
đế
n máy ch
ủ
), khi
đ
ó, m
ộ
t l
ệ
nh ng
ắ
t ti
ế
n trình
đ
ang
đượ
c th
ế
t qu
ả
c
ủ
a h
ệ
th
ố
ng s
ẽ
hi
ể
n th
ị
cho ng
ườ
i
dùng th
ấ
y
đượ
c k
ế
t qu
ả
c
ủ
a bài toán mà h
ệ
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Tr
ươ
ng Anh Hoàng GV
Đ
HD: TS. Ph
ạ
m Ng
ọ
c Hùng
Ch
ươ
ng 4. Ph
ươ
ng h
ướ
ng gi
ả
i quy
ế
t v
ấ
n, vì v
ậ
y c
ầ
n có ph
ươ
ng
th
ứ
c k
ế
t n
ố
i phù h
ợ
p v
ớ
i nh
ữ
ng yêu c
ầ
u
đ
ã
đượ
c nêu ra trong ph
ầ
n trên. Có hai
ph
ươ
ặ
c s
ử
d
ụ
ng k
ế
t n
ố
i socket.
Đố
i v
ớ
i ph
ươ
ng th
ứ
c k
ế
t n
ố
i d
ự
a trên webservice, th
ờ
i gian k
ế
t n
ố
ố
i
socket, ta ph
ả
i t
ự
xây d
ự
ng cách th
ứ
c giao ti
ế
p gi
ữ
a máy tr
ạ
m v
ớ
i máy ch
ủ
và máy ch
ủ
v
ớ
i máy khách.
Do yêu c
ầ
u t
ố
ự
ng giao ti
ế
p qua k
ế
t n
ố
i socket.
4.2. L
ự
a ch
ọ
n ngôn ng
ữ
l
ậ
p trình
Do ph
ươ
ng th
ứ
c k
ế
t n
ố
i
đượ
c l
ự
a ch
p gi
ữ
a máy ch
ủ
-
máy tr
ạ
m và máy ch
ủ
- máy khách. M
ặ
t khác, do các b
ộ
gi
ả
i có th
ể
đượ
c cài
đặ
t trên
nhi
ề
u n
ề
n h
ệ
đ
ế
t
đị
nh
s
ử
d
ụ
ng ngôn ng
ữ
l
ậ
p trình Java
để
xây d
ự
ng h
ệ
th
ố
ng.
4.3. Xác
đị
nh d
ữ
li
ệ
u
đầ
u vào,
d
ụ
ng nhi
ề
u
các b
ộ
gi
ả
i khác nhau. Tuy r
ằ
ng m
ỗ
i b
ộ
gi
ả
i có m
ộ
t chu
ẩ
n
đầ
u vào riêng, nh
ư
ng
để
ti
ệ
ẩ
n c
ủ
a SMT-LIB. Hi
ệ
n nay, h
ầ
u h
ế
t các công c
ụ
gi
ả
i các bài toán
đề
u h
ỗ
tr
ợ
chu
ẩ
n SMT-LIB, vì v
ậ
y,
để
tránh vi
ệ
c ph
ả
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
2010 Trang 18
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
Đ
H Công ngh
ệ
-
Đ
ề
u ki
ệ
n xây d
ự
ng m
ộ
t bài
toán d
ướ
i quy ch
ẩ
n c
ủ
a SMT-LIB.
H
ệ
th
ố
ng
đượ
c chia ra thành ba thành ph
ầ
n v
ớ
i ch
ứ
c n
ă
ng và vai trò khác nhau,
ủ
a h
ệ
th
ố
ng con
đ
ó.
V
ớ
i h
ệ
th
ố
ng
đượ
c cài
đặ
t trên máy khách, ng
ườ
i dùng s
ẽ
đư
a vào t
ệ
p tin ch
ứ
a
bài toán SMT ho
k
ế
t qu
ả
.
Đố
i v
ớ
i h
ệ
th
ố
ng
đượ
c cài
đặ
t trên máy ch
ủ
,
đầ
u vào nh
ậ
n t
ừ
máy khách (bài
toán SMT) s
ẽ
là
đầ
ể
n t
ớ
i máy khách.
Trên máy tr
ạ
m có duy nh
ấ
t m
ộ
t b
ộ
d
ữ
li
ệ
u
đầ
u vào là bài toán SMT nh
ậ
n
đượ
c
t
ừ
máy ch
ủ
và m
ộ
t b
ả
i bài toán SMT hi
ệ
u n
ă
ng cao – Ph
ầ
n máy tr
ạ
m
2010 Trang 19
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Tr
ươ
ng Anh Hoàng GV
Đ
HD: TS. Ph
ạ
ố
ng hoàn toàn
đượ
c xây d
ự
ng b
ằ
ng ph
ươ
ng pháp k
ế
t n
ố
i socket, vì v
ậ
y
c
ầ
n ph
ả
i có m
ộ
t cách th
ứ
c giao ti
ế
p phù h
ợ
p gi
ữ
ụ
ng
các th
ẻ
đươ
c quy
đị
nh s
ẵ
n
để
giao ti
ế
p gi
ữ
a các h
ệ
th
ố
ng con v
ớ
i nhau.
Các th
ẻ
s
ẽ
đượ
c
Th
ẻ
đ
óng s
ẽ
có d
ạ
ng <
/tên thẻ
>
Đố
i v
ớ
i th
ẻ
đơ
n thì không c
ầ
n có th
ẻ
đ
óng.
C
ụ
th
ể
ắ
t tay k
ế
t n
ố
i gi
ữ
a các thành ph
ầ
n trong
h
ệ
th
ố
ng v
ớ
i nhau.
-
C
ặ
p th
ẻ
<
file
> <
/file
>: th
ể
hi
ng
-
C
ặ
p th
ẻ
<result> </result>: th
ể
hi
ệ
n n
ộ
i dung k
ế
t qu
ả
c
ủ
a bài toán SMT
đượ
c
tr
ả
v
ề
-
Th
n <
exit
>: th
ể
thi
ệ
n s
ự
k
ế
t thúc k
ế
t n
ố
i gi
ữ
a ng
ườ
i dùng v
ớ
i máy ch
ủ
Copyright: Tài liệu đại học ©