Khóa luậ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
ĐẠ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àng
Cán bộ đồng hướng dẫn: TS. Phạm Ngọc Hùng
HÀ NỘI - 2010
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
Lời cảm ơn
Trước hết, tôi xin gửi lời cảm ơn chân thành và sâu sắc đến Tiến sỹ Trương
Anh Hoàng và Tiến sỹ Phạm Ngọc Hùng, những người đã trực tiếp hướng dẫn tôi
trong suốt quá trình nghiên cứu và phát triển đề tài nghiên cứu này. Để có được
những kết quả nghiên cứu như hiện nay, tôi vô cùng biết ơn sự quan tâm, hướng dẫn
nhiệt tình của hai thầy trong thời gian vừa qua.
Tôi xin chân thành cảm ơn các thầy cô trong trường Đại học công nghệ, Đại
học Quốc Gia Hà Nội nói chung, và các thầy cô trong khoa công nghệ thông tin nói
riêng, những người đã nhiệt tình giảng dạy, giúp tôi có những kiến thức quý báu để tôi
có thể hoàn thành được đề tài luận văn này.
Tôi xin bày tỏ lòng cảm ơn đến các anh chị cao học, và các bạn trong nhóm
nghiên cứu đã cùng tôi tìm hiểu và xây dựng hoàn chỉnh hệ thống giải quyết bài toán
Satisfiability Modulo Theories (SMT) với hiệu năng cao, giúp tôi có thể hoàn thành tốt
phần nghiên cứu của mình.
Và cuối cùng, tôi xin gửi lời cảm ơn đến gia đình, bạn bè và những người thân đã
bên cạnh, động viên giúp tôi hoàn thành tốt luận văn của mình.
Hà Nội, tháng 05/2010
Hoàng Thế Tùng
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
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
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ả.
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
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
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
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
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
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
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
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
Danh sách các bảng trong tài liệu
Bảng 1: Luật sinh một toán hạng................................................................................................7
Bảng 2: Luật sinh một công thức................................................................................................8
Bảng 3: Luật sinh một thuyết .....................................................................................................8
Bảng 4: Luật sinh một logic .......................................................................................................8
Bảng 5 Luật sinh một chuẩn.......................................................................................................9
Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2 ...............................................9
Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2..............................................10
Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm...............................................................37
Bảng 9: Kết quả thời gian của thực nghiệm .............................................................................37
Bảng 10: Kêt quả trả về của thực nghiệm ................................................................................38
Danh sách các hình trong tài liệu
Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao. ...............................................12
Hình 3.2: Mô hình ca sử dụng của hệ thống............................................................................14
Hình 3.3: Mô hình hoạt động của hệ thống.............................................................................15
Hình 5.1: Biểu đồ lớp của hệ thống máy trạm.........................................................................30
Danh sách từ viết tắt trong tài liệu
Từ viết tắt
Từ chuẩn
Diễn giải
Các lý thuyết module về
tính thỏa được
SMT
SMT-LIB
API
Satisfiability Modulo Theories
Satisfiability Modulo Theories -
Liblary
Thư viện các lý thuyết
module về tính thỏa được
Giao diện lập trình ứng
dụng
Application Programming
Interface
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
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
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
trong ngành khoa học máy tính cần đến những công thức logic phức tạp. Trong
khoảng hai thập niên gần đây, ngành khoa học máy tính đã có những tiến bộ lớn đối
với việc tự động chứng minh hay bác bỏ tính đúng đắn của một biểu thức logic. Tuy
nhiên việc chứng minh các biểu thức logic sẽ khó khăn hơn nhiều nếu đặt chúng trong
một nền lý thuyết thay vì chứng minh một cách tổng quát [1,2]. Những vấn đề này
được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories
hay còn được viết tắt là SMT [1]).
Cho đến nay, nhiều trường đại học cùng những nhà nghiên cứu khoa học máy
tính đã có những nghiên cứu, sản phẩm để giải quyết vấn đề này. Tuy nhiên, việc xây
dựng một bộ giải các vấn đề SMT tối ưu cho mọi trường hợp và rất khó khăn. Vì vậy,
vấn đề được đặt ra là kết hợp các bộ giải SMT đó để có được một bộ giải tối ưu nhất
về mặt thời gian.
1.2.Bài toán đặt ra
Đối với việc giải quyết các vấn đề SMT, nhiều trường đại học cũng như các cơ
quan, tổ chức lớn trên thế giới đã có những nghiên cứu và đưa ra những sản phẩm của
mình. Tuy nhiên, với mỗi sản phẩm, họ đưa vào những thuật toán khác nhau để giải
quyết vấn đề này. Trong khuôn khổ đồ án, việc nghiên cứu cơ chế, và tính đúng đắn
của những bộ giải này không được đề cập đến (kết quả đưa ra của các bộ giải sẽ được
coi là luôn đúng đắn) mà sẽ tập trung vào việc sử dụng những bộ giải này như là
những công cụ giải quyết vấn đề SMT được đưa vào. Với những kết quả đưa ra bởi
các bộ giải này, cần có một kết trả được trả về tối ưu nhất về mặt thời gian.
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
Trang 1
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
Để giải quyết vấn đề nói trên, cần có một hệ thống phân phối các vấn đề SMT
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.
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
Trang 2
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
Chương 2. Kiến thức nền tảng
2.1.Giới thiệu SMT
Tính thỏa mãn là một trong những vấn đề quan trọng nhất của ngành khoa học
máy tính. Các vấn đề cần tính thỏa mãn được ứng dụng trong cả phát triển phần cứng
cũng như phần mềm, đặc biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị [3].
Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây dựng dựa trên việc
tạo ra các công thức tiền tố và việc chứng minh tính hợp lệ của chúng. Cho dù hai thập
niên gần đây, việc chứng minh tính hợp lệ của các định lý, biểu thức tiền tố có những
tiến bộ đáng kể, tuy nhiên, không phải công thức nào cũng có thể chứng minh một
cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều công thức không quan tâm
đến tính khả thi trong trường hợp tổng quát mà chỉ được quan tâm trong một lý thuyết
nền tảng [2,1]. Việc nghiên cứu tính khả thi của các công thức trong một lý thuyết nền
tảng được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo
Theories hay SMT) và các công cụ để chứng minh một cách tự động các tính khả thi
của những vẫn đề SMT được gọi là bộ giải SMT (SMT solver).
Lý thuyết về SMT sẽ được đề cập cụ thể hơn trong phần giới thiệu về thư viện
SMT.
2.2.Bộ giải SMT (SMT solver)
Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT được phát triển khá
sớm, từ đầu những năm 1980. Tại thời điểm đó, một số bộ giải được xây dựng bởi
Greg Nelson và Derek Oppent tại trường đại học Stanford , Robert Shostak tại SRI, và
Robert Boyer và J Moore tại trường đại học ở Texas. Đến cuối những năm 1990, việc
nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ SAT đã xây dựng nhiều bộ
giải SMT tiến bộ hơn [4].
Như đã đề cập ở trên, trong khuôn khổ đồ án, việc đánh giá về tính đúng đắn,
các nghiên cứu về thuật giải của từng bộ giải sẽ không được đề cập đến. Vấn đề được
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
Trang 3
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
đặ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 đề
SMT-LIB đều được sử dụng bởi chuẩn 1.2 mà họ đã xây dựng vào khoảng tháng 8
năm 2006.
2.3.1. Cấu trúc cơ bản của SMT-LIB
Như đã nói ở trên, vấn đề SMT là việc kiểm tra biểu thức logic φ có thỏa mãn
được hay không trong lý thuyết nền T hay có một khuôn mẫu của T là khả thi. Vì vậy,
kiến trúc cơ bản của một SMT-LIB thường bao gồm các vấn đề sau [7]:
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
Trang 4
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
- Một thủ tục logic cơ sở (underlying logic): Định dạng SMT-LIB hiện tại có hai
định nghĩa về ngữ nghĩa của logic cơ sở. Thứ nhất là dịch nghĩa sang những
biểu thức tiền tố cổ điển, có nghĩa là thủ tục của logic cơ sở giúp cho việc
chuyển đổi sang khung làm việc của công cụ có sẵn hoặc giúp kiểm tra kết quả
một cách dễ dàng hơn. Nghĩa thứ hai là chi phối ngữ nghĩa đại số dựa trên
nhiều khuôn mẫu rút gọn.
- Một lý thuyết nền (background theory): là những lý thuyết nền dùng để kiểm
chứng tính thỏa mãn. Những lý thuyết cơ bản bao gồm lý thuyết số thực, lý
thuyết mảng.. Phiên bản hiện tại của SMT-LIB chỉ hỗ trỡ những lý thuyết cơ
bản này.
- Một ngôn ngữ đầu vào (input language): Là lớp các biểu thức được chấp nhận
như là đầu vào của SMT-LIB.
2.3.2. Khuôn dạng của SMT-LIB
Một thư viện SMT được xây dựng theo chuẩn và dựa trên những định nghĩa sau
(theo [7]):
Định nghĩa 1 (Ký hiệu của SMT-LIB – SMT-LIB signature): Một ký hiệu SMT-
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)
⊆ ͊;
S
- Một toàn ánh (total mapping) từ các biến (term variables) X tới Σ ;
F
S +
- Một quan hệ toàn phương (total relation) từ Σ đến (Σ ) , một chuỗi các
S
thành phần của Σ , không bao giờ có một cặp định dạng (f,s1…sns) và
(f,s1…sns’) với s và s’ khác nhau;
P
S
P
- Một quan hệ toàn phương từ Σ tới (Σ )*, thứ tự các thành phần Σ .
Định nghĩa 2 (Công thức trong SMT-LIB – SMT-LIB formula): Các công thức
trong ngôn ngữ SMT-LIB là một tập hợp tất cả các công thức đúng cú pháp
đóng (closed well-formed formula).
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
Trang 5
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
Định nghĩa 3 (khai báo lý thuyết – theory decl): chỉ tồn tại một khai báo lý
thuyết trong một bài toán SMT-LIB và phải thỏa mãn những giới hạn sau:
- Chúng bao gồm các khai báo của thuộc tính “sort” và “definition”;
- Chúng chứa ít nhất một khai báo với một thuộc tính;
- Không tồn tại khai báo định dạng f,s1…sns và f,s1…sns’ 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 DT 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 DL trong SMT-LIB;
- Mỗi một ký hiệu được khai báo trong thuộc tính “extrasorts”, “extrafuns”
và “extrapred” cần phải là một phần của các ký hiệu được định nghĩa trong
thuộc tính “language” của logic L;
- Có thể có hơn một khai báo của thuộc tính “extrasort”;
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
Trang 6
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
- Có thể có hơn một khai báo của thuộc tính “extrafuns”, và mỗi thuộc tính
“funs” của khai báo thuyết liên kết tới DL phải thỏa mãn yêu cầu 3 của
định nghĩa 3;
- Ký hiệu rút gọn trong khai báo “extrafuns” hoặc “extrapred” hoặc được
khai báo trong “extrasort” hoặc thuộc về ký hiệu của logic L;
- Công thức trong khai báo thuộc tính “assumption” và “formula” là ngôn
ngữ của L và các ký hiệu của chúng được khai báo trong thuộc tính
“extrasorts” “extrafuns” và “extrapred”.
Từ những định nghĩa trên, việc xây dựng một bài toán SMT dựa trên chuẩn
SMT-LIB sẽ theo cấu trúc sau [7]:
Bảng 1: Luật sinh một toán hạng
(1) < simple_identifier>
::= Chuỗi các ký tự, số, dấu chấm(.), nháy đơn(‘)
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>
(4) <numeral>
(5) <rational>
(6) <indexed_identifier>
(7) <identifier>
(8) <var>
::= {< user_value_content>}
::= 0 | chuỗi không rỗng các chữ số bắt đầu khác 0
::= <numeral>.0*<numeral>
::= < simple_identifier>[<numeral>(:<numeral>)*]
::= <simple_identifier> | <indexed_identifier>
::= ?< simple_identifier >
(9) <fvar>
::= $< simple_identifier >
(10) <attribute>
(11) <arith_symb>
::= : <simple_identifier>
::= Chuỗi không rỗng các ký tự:
=, >, <, &, @, #, +, -, *, /, %, |, ~
(12) <funs_symb>
(13) <pred_symb>
(14) <sort_symb>
(15) <annotation>
(16) <base_term>
(17) <an_term>
::= <identifier> | <arith_symb>
::= <identifier> | <arith_symb> | distinct
::= <identifier>
::= <attribute> | <attribute> < user value>
::= <var> | <numeral> | <rational> | <identifier>
::= <base_term> | (<base_term> <annotation>+)
| (<funs_symb> <an_term>+ <annotation>*)
| (ite <an_formula> <an_terrm> <an_term>
<annotation>*)
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
Trang 7
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
Bảng 2: Luật sinh một công thức
(1) <prop_atom> ::= true | false | <fvar> | <identifier>
(2) <an_atom>
::= <prop_atom> | ( <prop_atom> <annotation>+)
| (<pred_symb> <an_term>+ <annotation>*)
(3) <connective> ::= not | implies | if_then_else | and | or | xor | iff
(4) <quant_symb> ::= exists | forall
(5) <quant_var>
(6) <an_formula> ::= <an_atom>
| ( <connective> <an formula>+ <annotation>* )
(<quant_symb> <an_formula>
<quant_var>+
<annotation>* )
::= ( <var> <sort_symb>)
|
| (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>
(2) <string>
(3) <fun_symb_decl>
::= chuỗi liên tiếp các ký tự
::= “<string_content>”
::= (<func_symb> <sort_symb>+ <annotation>*)
| (<numeral> <sort_symb> <annotation>*)
| (<rational> <sort_sumb> <annotation>*)
(4) <pred_symb_decl> ::= (<pred_symb> <sort_symb>* <annotation>*)
(5) <theory_name>
(6) <theory_attribute>
::= <identifier>
::= :sort ( <sort_symb>+)
| :funs (<fun_symb_decl>+)
| :preds (<pred_symb_decl>)
| :definition <string>
| :axioms <string>
| <annotation>
(7) <theory>
::= (theory <theory_name> <theory_atrribute>+)
Bảng 4: Luật sinh một logic
(1) <logic_name>
::= <identifier>
(2) <logic_attribute>
::= : theory <theory_name>
| :language <string>
| :extensions <string>
| :notes <string>
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
Trang 8
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
| <annotation>
(3) <logic>
::= (logic <logic_name> <logic_attribute>+)
Bảng 5 Luật sinh một chuẩn
(1) <status>
(2) <bench_name>
(3) <bench_attribute>
::= sat | unsat | unknown
::= <identifier>
::= :logic <logic_name>
| :assumption <an_formula>
| :formula <an_formula>
| :status <status>
| :extrasorts ( <sort_symb>+ )
| :extrafuns ( <fun_symb_decl>+ )
| :extrapreds ( <pred_symb_decl>+ )
| :notes <string>
| <annotation>
(4) benchmark
::= ( benchmark <bench_name> <bench attribute>+ )
Các lý thuyết nền cơ bản đã được nghiên cứu và đưa ra:
Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2
Các hàm mảng
Arrays
Các hàm mảng mở rộng
ArraysEx
Bit vector 32 bit
Fixed_Size_BitVectors[32]
Fixed_Size_BitVectors
BitVector_ArraysEx
Bit vector với kích cỡ tùy ý.
Bit vector với kích cỡ tùy ý và mảng chứa kiểu
dữ liệu bit vector
Thuyết trống với ký hiệu rỗng
Số nguyên
Empty
Ints
Mảng số nguyên
Int_Arrays
Int_ArraysEx
Mảng giá trị được đánh thứ tự số nguyên với tiền
đề mở rộng
Mảng của mảng các số nguyên và số thực với tiền
đề mở rộng
Int_Int_Real_Array_ArraysEx
Số thực
Reals
Số nguyên và số thực
Reals_Ints
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.
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
Trang 9
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
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
Các công thức tuyến tính trên thuyết mảng số nguyên với
những ký tự phân cấp, hàm và thuộc tính tự do.
Các công thức tuyến tính với ký hiệu hàm và ký hiệu vị từ
trong thuyết 10 nêu trên
AUFLIA
AUFLIRA
Công thức với các ký tự hàm và vị từ tự do dựa trên thuyết 10
Công thức tuyến tính trên các phép toán số nguyên
Công thức tuyến tính trên các phép toán số thực
Công thức lượng từ tự do trên thuyết mảng không mở rộng
Công thức lượng tự trên thuyết bitvector và mảng bitvector với
các ký hiệu hàm và ký hiệu vị từ tự do.
AUFNIRA
LIA
LRA
QF_A
QF_AUFBV
Công thức tuyến tính và lượng từ tự do trên thuyết mảng các số
nguyên với ký tự phân cấp, ký tự hàm và ký tự lượng từ.
Công thức lượng từ tự do trên thuyết của mảng mở rộng
Công thức lượng từ tự do với thuyết bitvector cố định kích cỡ
Logic khác trên số nguyên. Ví dụ bất đẳng thức x-y <b với x,y
là các biến nguyên và b là một hằng số nguyên
Tổ hợp giữa bất đẳng thức của đa thức tuyến tính trên biến số
nguyên
QF_AUFLIA
QF_AX
QF_BV
QF_IDL
QF_LIA
Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số thực
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
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_LRA
QF_NIA
QF_RDL
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
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_UF
QF_UFIDL
QF_UFBV
QF_UFLIA
QF_UFLRA
QF_UFNRA
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ừ.
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ừ
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ừ
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ừ
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
Trang 10
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
Phép tính số nguyên không tuyến tính với ký tự phân cấp, hàm
và vị từ không xác định.
UFNIA
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
Trang 11
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
Chương 3. Phân tích hệ thống
3.1.Mô hình hệ thống
Để giải một bài toán SMT một cách song song giữa các bộ giải, đồng thời đảm
bảo được hiệu năng cao cho hệ thống, nhóm nghiên cứu đã đưa ra hướng giải quyết là
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 đề
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
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
t
ừ
nhiều người sử
cho tất cả các bộ giải và chờ đợi kết quả trả
cho phía yêu cầu. Đối với những bộ giả đưa ra kết quả sau sẽ nhậ
lý vấ đề đó. Do hệ thống được xây dựng trực tuyến, nên việc nhận cùng một lúc
nhiều yêu cầu cần xử lý là
chia một vấ đề cho nhiều máy trạm xử lý, vừa phải xử lý đồng thời cùng lúc nhiề
yêu cầu như
d
ụng trực tuyến. Với mỗi vấ
n
đề nhậ
n
được, hệ thống sẽ phân phố
ặt thời gian để trả
được tín hiệu dừng
i
v
ề
t
ố
i
ưu nhất về
m
v
ề
i
n
x
ử
n
đ
i
ều tất yếu, vì vậy, hệ thống máy chủ
v
ừa
đảm nhận việ
c
n
u
v
ậ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
ột lúc và phải trả ết quả tương ứng cho mỗi vấ đề. Để tiện cho người sử
ụng bên phía máy khách, hệ thống cần phải có một thư việc các hàm nhúng API để
ụng trực tiếp xây dựng vấ đề SMT và gửi lên phía máy chủ
v
d
ấ
n
đề
m
v
ề
k
n
người sử
d
n
.
3.2.Mô hình ca s
ử
d
ụng c
ủ
a hệ
th ng
ố
Đối với hai hệ thống con được cài đặt trên máy khách và máy trạm, thì máy chủ
đượ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.
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 13
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
Hình 3.2: Mô hình ca sử dụng của hệ thống
Ở phía máy khách (user), người sử dụng sẽ tạo bài toán SMT, hoặc chỉ định cho
hệ thống tệp tin SMT cần thiết phải kiểm tra tính thỏa mãn để hệ thống sẽ gửi lên phía
máy chủ (server). Sau khi gửi bài toán lên phía máy chủ, hệ thống trên máy khách sẽ
chờ cho máy chủ gửi kết quả về và nhận kết quả trả về. Viêc gửi bài toán SMT bên
phía máy khách sẽ bao gồm cả việc gửi yêu cầu thời gian ngắt của các bộ giải SMT.
Với máy trạm (solver) sau khi kết nối và nhận được tệp tin chứa vấn đề SMT
cần giải quyết, hệ thống sẽ gọi lệnh chạy các công cụ giải SMT. Sau khi đưa ra được
kết quả, hoặc sau khi nhận được tín hiệu ngắt từ phía máy chủ, máy trạm sẽ gửi lại kết
quả đến máy chủ để máy chủ gửi lại phía máy khách.
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
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
3.3.Mô hình hoạt độ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:
Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN
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
Khi hệ thống hoạ
toán SMT. Bài toán SMT có thể đã được mô tả
chương trình với việc sử ụng hệ thống được cài đặt trên. Sau khi xác định bài toán
SMT, hệ thống máy khách sẽ ửi bài toán toán đó cho máy chủ đồng thời gửi thông tin
thời gian giới hạn thực hiện giải bài toán và chờ đợi kết quả trả phía máy chủ
t
động, các máy khách sẽ
k
ết nố
i
đến máy chủ và xây dựng bài
b
ằng tệp tin hay được xây dựng bằng
d
g
v
ề
v
ề
từ
.
Máy chủ
tham số thời gian thực hiện bài toán gửi từ máy khách, máy chủ
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ố
và đón chờ ết quả phản hồi từ máy trạm.
l
ắng nghe các kết nối của máy khách, khi nhậ
n
được bài toán SMT và
v
ề
sẽ
phân phối các
i
đến máy chủ
k
Máy trạm sẽ nhận bài toán từ máy chủ và bắ
khi đó giá trị
máy trạm gọi các bộ giả
ra tiếp sau đó. Trường hợp một là máy trạ
phía máy chủ
có máy trạm khác gử
đang được thực thi sẽ được gọi. Và
máy chủ ữa.
t
đầu việc thực hiện giải bài toán,
v
ề
trễ thời gian cho mỗi bài toán sẽ được sử
d
ụng. Sau khi hệ thống trên
đề được đưa tới, sẽ có hai trường hợp xả
đó sẽ giải ra kết quả nhanh nhất và gửi về
được tín hiệu ngắt tiến trình (do
được kết quả đến máy chủ), khi đó, một lệnh ngắt tiến trình
trường hợp này, máy trạm không gửi gì về phía
i
để giải quyết vấ
n
y
m
k
ết quả. Trường hợp thứ hai là nhậ
n
đ
ã
i
ở
n
Phía máy khách sau khi nhậ
n
được kết quả
c
ủa hệ thống sẽ hiển thị cho người
đến.
dùng thấ được kết quả ủa bài toán mà hệ thống gửi
y
c
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 16
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
Chương 4. Phương hướng gi
ải quy
ế
t v
ấn
đề
4.1.L
ự
a chọn phương th
ứ
c kết nố
i
Bài toán được đặt ra là xây dựng hệ thống trực tuyế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ầ được nêu ra trong phần trên. Có hai
phương thức kết nố được đưa ra lựa chọn là xây dựng hệ thống dựa trên các kết nố
ủa webservice hoặc sử ụng kết nối socket.
u
đ
ã
i
i
c
d
Đối với phương thức kết nối dựa trên webservice, thời gian kết nối sẽ chậm hơ
n
r
ất nhiều so với kết nối trực tiếp qua socket. Tuy nhiên, với phương thức kết nố
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ủ
ới máy khách.
i
v
Do yêu cầu tố
i
ưu về
mặt thời gian được quan tâm hàng đầu, vì vậy phương
thức
được tố ưu cho hệ thống là xây dựng giao tiếp qua kết nối socket.
i
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ọn là kết nối socket, vì vậy cần một ngôn
ngữ
lập trình bậc cao để tiện cho việc xây dựng cách thức giao tiế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ệ điều hành khác nhau, nên cần có ngôn ngữ ập trình hỗ trợ việc chạy trên
nhiều hệ điều hành khác nhau. Chính vì các lý do này, nhóm nghiên cứ đã quyế định
ụng ngôn ngữ ập trình Java để xây dựng hệ thống.
l
u
t
sử
d
l
4.3.Xác định d
ữ
li
ệu
đầu vào, đầu ra c
ủ
a hệ
th ng
ố
Để
t
ăng hiệu năng của hệ thống giải bài toán SMT, hệ thống có sử
các bộ giải khác nhau. Tuy rằng mỗi bộ giải có một chuẩ đầu vào riêng, nhưng để
tiện cho việc giải quyết vấ đề ột cách nhanh chóng và hiệu quả, hệ thống chỉ
ụng đầu vào bài toán SMT theo chuẩ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ải chuẩn hóa đầu
vào cho mỗi bài toán nhằ đảm bảo hiệu năng cao về ặt thời gian, hệ thống yêu cầ
dụng nhiều
n
n
m
s
ử
d
m
m
u
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 17
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
đầu vào của người sử
d
ụng phả
i
đáp ứng nghiêm ngặt các
điề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,
do đó với mỗi hệ thống con sẽ có mộ đầu vào đầu ra riêng ứng với từng chức năng
ủa hệ thống con đó.
t
c
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ứ
bài toán SMT hoặc xây dựng bài toán SMT dựa trên các hàm nhúng API mà hệ thống
xây dựng. Bài toán sẽ được gửi lên máy chủ và chờ máy chủ phản hồi về ết quả
a
k
.
Đố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à đầu ra chuyển tới máy trạm. Và đầu vào thứ hai là kết quả nhậ
n
được
t
ừ
ừ
máy trạm cũng là đầu ra để chuyể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ộ liệ đầu ra duy nhất là kết quả
d
ữ
u
c
ủa việc giải bài toán SMT
đó.
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 18
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
Chương 5. Mô t
ả
hệ
th ng
ố
Hệ thống giải bài toán SMT hiệu năng cao được chia làm ba hệ thống con với chức
năng và tác dụng riêng. Trong giới hạn tài của tài liệu này, hệ thống con cài đặt trên
máy chủ sẽ không được đề cập đến. Trong phần này, hệ thống cài đặt trên máy khách
và máy trạm sẽ đươc giải thích và mô tả chi tiết.
5.1.Quy định cách th
ứ
c giao ti
ếp v
ớ
i máy ch
ủ
Do hệ thống hoàn toàn được xây dựng bằng phương pháp kết nối socket, vì vậ
ần phải có một cách thức giao tiếp phù hợp giữa các hệ thống con với nhau. Dựa trên
ý tưởng của ngôn ngữ XML, nhóm nghiên cứ đưa ra và thống nhất việc sử ụng
các thẻ đươc quy định sẵ để giao tiếp giữa các hệ thống con với nhau.
y
c
u
đ
ã
d
n
Các thẻ sẽ được định nghĩ
a
đúng như quy chuẩn của XML với quy định sau:
- Thẻ có dạng <tên thẻ
m
ở
s
ẽ
>
- Thẻ đóng sẽ có dạng </tên thẻ
Đối với thẻ đơn thì không cần có thẻ đóng.
thể, các thẻ được quy định trong hệ thống như sau:
>
C
ụ
- Cặp thẻ
thống với nhau.
- Cặp thẻ file> </file>: thể hiện việc bắ
<
hello> </hello> : thể hiện sự bắt tay kết nối giữa các thành phần trong
h
ệ
<
t
đầu chuyển dữ liệu từ tệp tin chứa bài
toán SMT giữa các hệ thống con trong hệ thống
- Cặp thẻ <result> </result>: thể hiện nội dung kết quả
c
ủa bài toán SMT được
trả
- Thẻ đơn <destroy>: là tín hiệu ngắt kết nố
- Thẻ đơn <exit>: thể thiện sự
v
ề
i
được máy chủ
g
ử
i
đến máy trạm
k
ết thúc kết nối giữa người dùng với máy chủ
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 19
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
5.2.Ph n máy khách
ầ
5.2.1. Quy định giao tiếp với máy chủ
Yêu cầu chính cho hệ thống cài đặt trên máy khách là gửi bài toán SMT và
nhận về
k
ết quả
của bài toán ấy. Quy trình kết nối của máy khách với máy chủ
sẽ
như sau:
- Sau khi kết nố được máy chủ, máy khách sẽ đưa ra một loạt thẻ chào hỏi
i
<hello>
[Name]
</hello>
- Sau chuỗi các thẻ được gửi lên máy chủ, máy khách sẽ chờ đến khi máy chủ
đáp lại “OK”. Sau đó, hệ thống trên máy khách sẽ thực hiện tiến trình gửi trễ
thời gian (time out) giải bài toán SMT cần giải. Trễ thời gian này được người sử
d
ụng quy định và đưa vào.Trong trường hợp người dùng không thiết lập thông
tin này, thì hệ thống sẽ ửi lên thời gian mặ định là 30 giây. Quá trình gửi trễ
g
c
thời gian được quy định như sau:
<timeout>
[trễ thời gian]
</timeout>
- Sau khi gửi lên thời gian giới hạn thực thi của bài toán, hệ thống sẽ tiếp tục gử
i
lên tệp tin dữ liệu chứa nội dung bài toán. Quy trình gửi tệp tin dữ liệu cũng
được theo quy định sau:
<file>
[Nội dung dữ liệu chuyển lên]
</file>
- Sau quá trình gửi tệp tin dữ liệu thành công, hệ thống trên máy khách chờ
k
ết
quả
của máy chủ trả
v
ề. Khi nhậ
n
được tín hiệu trả
v
ề
( tín hiệu kết quả trả
v
ề
được quy định là thẻ
m
ở
<result>) hệ thống sẽ nhận cho đến khi có tín hiệu kết
thúc (thẻ đóng </result>):
<result>
[nội dung kết quả trả về]
</result>
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 20
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
- Sau khi đã nhậ
chủ
Như đã đề
chuẩn hóa đầu vào, hệ thống yêu cầu người sử
chuẩn của SMT-LIB. Vấ đề đặt ra ở đây là không phải lúc nào người sử
ũng có sẵn bài toán SMT được tổ chức theo quy chuẩn của STM-LIB. Chính
vì vậy, hệ thống cần phải xây dựng các hàm API để người dùng có thể xây
ựng bài toán theo đúng chuẩ định dạng của SMT-LIB.
n
được kết quả, máy khách sẽ chủ động ngắt kết nối đến máy
.
c
ập
ở
trên, để tránh việc lãng phí thời gian của hệ thống cho việ
ụng đưa vào đầu vào theo đúng
ụng
c
d
n
d
c
d
n
D
ựa vào các định nghĩa và quy chuẩn về đầu vào của bài toán SMT theo chuẩ
SMT-LIB (được nêu trong phần kiến thức nền tảng), hệ thống đưa ra các hàm API
để thuận tiện cho người sử ụng đưa vào.
n
đ
ã
d
5.2.2. Các lớp của hệ thống máy khách
5.2.2.1. Lớp config: ớp này được xây dựng để chứa các quy ước việ
giao tiếp cũng như các thành phần mặ định của hệ thống như các thẻ
tên tệp tin đầu vào mặ định, thời gian ngắt mặ
liệ được trả
5.2.2.2. Lớp Client: Có chức năng mở
máy chủ và nhận về ết quả
5.2.2.3. Lớp NetSolver: bao gồm các hàm thiết lập tùy chọn cho người sử
ụng. Cụ thể
void setPath (String Path): Thiết lậ
Có thể là mộ đường dẫ đến một tệp tin sẽ được xây dựng sau đó bở
chính người sử ụng. Hoặc cũng có thể là một tệp tin đã chứa nộ
dung bài toán SMT cân gửi lên máy chủ
void setOutput (String Path): Thiết lậ đường dẫn cho tệp tin lưu giữ
ết quả được trả ề. Xin lưu ý rằng việc thiết lậ đường dẫn bao gồ
tên tệp tin.
void Solve (): thực thi việc gửi và nhận bài toán SMT. Thực chất hàm
này chỉ ọi mộ đối tượng của lớp Client và thực thi đối tượng ấy.
l
c
c
,
c
c
định, tên tệp tin chứ
a
d
ữ
u
v
ề
k
ết nối, gửi bài toán từ tệp tin lên
k
.
d
:
-
p
đường dẫn cho tệp tin đầu vào.
t
n
i
d
i
.
-
-
p
k
v
p
m
cả
g
t
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 21
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
Việc xây dựng bài toán SMT sẽ
ởi các lớp sau. Xin lưu ý rằng các hàm API được xây dựng hoàn
toàn dựa trên bộ luật cú pháp của ngôn ngữ đầu vào SMT được
đưa ra trên.
dựa trên các hàm API được xây dựng
b
đ
ã
ở
5.2.2.4. Lớp Bench_attribute: Được xây dựng dựa trên bảng 5.
-
Bench_attribute (String Bench_name)
:
Định nghĩa một thuộc tính
Benchmark đầu vào với tên là Bench_name.
Void setLogic (String LogicName): thiết lập tên logic của Benchmark
void setStatus (String stt) : thiết lập thuộc tính Status cho Benchmark
void setFormulas (Formula F): thiết lập Formula cho Benchmark.
void setAssumtion (Formula f): thiết lập Assumtion cho Benchmark
void setAnnotation (annotation an): thiết lập Annotation cho
Benchmark
-
-
-
-
-
-
-
void setNotes (String note): thiết lập Note cho Benchmark
void setExtrasorts (Identifier[] id): Thiết lập Extrasorts cho
Benchmark
-
-
-
void setExtrafuns (func_decl[] funcs): Thiết lập Extrafuns cho
Benchmark
void setExtrapreds (pred_decl[] preds): thiết lập Extrapreds cho
Benchmark
void printBench (): ghi Benchmark vừa thiết lập ra tệp tin được chỉ
định
5.2.2.5. Lớp Formula: Được xây dựng dựa trên bảng 2 để đưa ra các
công thức trong bài toán SMT, Các hàm hỗ trợ xây dựng bao gồm:
-
-
-
Formula (boolean b): khai báo một Formula với giá trị là giá trị
ột biến logic
c
ủ
a
m
Formula (fvarDecl fvar): Khai báo một Formula với giá trị là mộ
t
khai báo hàm.
Formula (Identifier id): khai báo một Formula với giá trị là mộ định
t
danh Identifier.
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 22
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
-
-
Formula (Identifier id, Term te[]): khai báo một Formula từ
danh Identifier và một mảng không rỗng các phần tử Term
m
ộ
t
định
Formula (Arith_symb ar, Term te[]): khai báo một Formula từ
m
ộ
t
(hoặc một chuỗi) các phép toán và một mảng không rỗng các phần tử
Term
-
-
Formula (Term te[]): khai báo một Formula với từ khóa “distinct” và
m
ột mảng không rỗng các phần từ Term
void Setvalue (String val): đặt giá trị ủa Formula theo tùy biến ( khi
ụng không thể xây dựng dựa trên các hàm
c
công thức của người sử
API trong lớp formula)
d
-
-
-
-
-
-
-
-
Formula orOperator (Formula a1, Formula a2): phép “or” giữa hai
công thứ
Formula xorOperator (Formula a1, Formula a2): phép “xor” giữa hai
công thứ
Formula iffOperator (Formula a1, Formula a2): phép “iff” giữa hai
công thứ
Formula impliesOperator (Formula a1, Formula a2): phép “implies”
giữa hai công thứ
Formula existsFomular (quant_var[] qv, Formula f): công thứ
xây dựng với từ khóa “exists
c
c
c
c
c
c
được
được
”
Formula forallFomular (quant_var[] qv, Formula f): công thứ
xây dựng với từ khóa “forall”
Formula letFormula (varDecl var,Term t, Formula f): công thứ
được xây dựng với từ khóa “let”
c
Formula fletFormula (fvarDecl fvar,Formula f1, Formula f2): công
thứ được xây dựng với từ khóa “flet
5.2.2.6. Lớp func_decl: khai báo một hàm của bài toán SMT, được xây
ựng dựa trên (3) bảng 3.
c
”
d
-
func_decl (double d, Identifier id): khai báo một hàm từ giá trị
thực và định danh Identifier
một số
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 23
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
-
-
func_decl (Identifier id1, Identifier[] id): khai báo một hàm từ giá trị
định danh Identifier và một mảng không rỗng định danh Identifier
mộ
t
func_decl (Arith_symb ar,Identifier[] id): khai báo một hàm từ
hoặc chuỗi các phép toán và mảng không rỗng các định danh id
m
ộ
t
5.2.2.7. Lớp pred_decl: khai báo một vị
ựng dựa trên (4) bảng 3
t
ừ
của bài toán SMT, được xây
d
-
-
-
pred_decl (Identifier[] id): khai báo một vị
t
ừ
v
ới giá trị của một dịnh
danh id
pred_decl (Arith_symb ar, Identifier[] id): khai báo một vị
t
ừ
t
ừ
m
ộ
ộ
t
t
(hoặc một chuỗi) các phép toán ar và một mảng các định danh id
pred_decl (Identifier id1, Identifier[] id): khai báo một vị
đinh danh id1 và mảng các định danh id
t
ừ
t
ừ
m
5.2.2.8. Lớp Term: được xây dựng dựa trên bảng 1.
-
-
-
-
Term (varDecl v): khái báo một term từ khai báo của một biến v
Term (double d): khai báo một term từ giá trị ủa một số thực d
Term (Identifier i): khai báo một term từ đinh danh i
c
mộ
t
Term iteOperator (Formula f, Term t1, Term t2): toán tử
“
ite” củ
a
Term
5.2.2.9. Lớp annotation: được xây dựng dựa trên (15) bảng 1, dùng để
khai báo một ghi chú trong bài toán SMT. Có hai cách khai báo như
sau:
-
-
annotation (String attribute): khai báo ghi chú với chuỗi ký tự
attribute
annotation (String attribute, String user_value): khai báo ghi chú vớ
i
chuỗi ký tự thuộc tính attribute và user_value
5.2.2.10. Lớp varDecl: Dùng để khai báo một biến trong bài toán SMT.
Được xây dựng dựa trên (8) bảng 1
-
varDecl (String v): khai báo biến với chuỗi v
5.2.2.11. Lớp fvarDecl: được xây dựng dựa trên (9) bảng 1.
fvarDecl (String fv): dùng để khai báo fvar với chuỗi fv
-
Sinh viên: Hoàng Th
ế
Tùng – K51CNPM – Khoa CNTT -
GV
Đ
H Công ngh
ệ
-
Đ
H QGHN
GVHD: TS. Trương Anh Hoàng
ĐHD: TS. Ph
ạ
m Ng c Hùng
ọ
Trang 24
Tải về để xem bản đầy đủ
47 trang
05/07/2025
80
Bạn đang xem 30 trang mẫu của tài liệu "Khóa luậ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", để tải tài liệu gốc về máy hãy click vào nút Download ở trên.
File đính kèm:
- khoa_luan_xay_dung_he_thong_giai_bai_toan_smt_hieu_nang_cao.pdf
