# 2. SMT-solvers ### 2.1 School-level system of equations 1 ví dụ về hệ phương trình cấp trường thpt:
Nó được giải quyết bằng z3py như sau: ```python #!/usr/bin/python from z3 import * x = Real('x') y = Real('y') z = Real('z') s = Solver() s.add(3*x + 2*y - z == 1) s.add(2*x - 2*y + 4*z == -2) s.add(-x + 0.5*y - z == 0) print s.check() print s.model() ``` Chúng ta sẽ nhận được kết quả: ``` sat [z = -2, y = -2, x =1] ``` Nếu chúng ta thay đổi bất kỳ phương trình nào đó để nó không có nghiệm thì `s.check()` sẽ trả về "unsat". Và cũng có thể được biểu diễn thông qua ngôn ngữ tiêu chuẩn cho SMT được gọi là SMT-LIB: ``` (declare-const x Real) (declare-const y Real) (declare-const z Real) (assert (=(-(+(* 3 x) (* 2 y)) z) 1)) (assert (=(+(-(* 2 x) (* 2 y)) (* 4 z)) -2)) (assert (=(-(+ (- 0 x) (* 0.5 y)) z) 0)) (check -sat) (get-model) ``` Đây là một ngôn ngữ rất gần với LISP (ngôn ngữ xử lý danh sách), nhưng sẽ hơi khó đọc đối với những người chưa qua đào tạo. Bây giờ chạy nó ta được: ```shell % z3 -smt2 example.smt sat (model (define-fun z () Real (- 2.0)) (define-fun y () Real (- 2.0)) (define-fun x () Real 1.0) ) ``` ### 2.2 Another school-level system of equations Chúng ta đã từng một lần gặp cái này trên Facebook:
Nó thật dễ dàng để giải quyết trong Z3: ```python #!/usr/bin/python from z3 import * circle , square , triangle = Ints('circle square triangle ') s = Solver() s.add(circle+circle==10) s.add(circle*square+square==12) s.add(circle*square -triangle*circle==circle) print s.check() print s.model() ``` ``` sat [triangle = 1, square = 2, circle = 5] ``` ### 2.3 Why variables are declared using `declare-fun`? ``` ... (declare-fun const1 () (_ BitVec 32)) (assert (= const1 (_ bv214013 32))) ... ``` ### 2.4 Connection between SAT and SMT solvers Bộ giải SMT là tiền đề cho bộ giải SAT, nghĩa là chúng dịch các biểu thức SMT đã nhập thành CNF và cung cấp cho bộ giải SAT với nó. Quá trình dịch thuật đôi khi được gọi là "bit blasting". Một số SMT-solvers sử dụng SAT-solver: STP sử dụng MiniSAT hoặc CryptoMiniSAT làm chương trình phụ trợ. Một số SMT-solvers (like z3) có SAT-solver riêng. ### 2.5 Referential transparency Điều này rất quan trọng - một biến chỉ có thể được gán một lần. Giống như trong Verilog/VHDL, Haskell. {% hint style="info" %} **Like in SSA (Static Single Assignment):** "One important property (thuộc tính) that holds for all varieties of SSA, including the simplest definition above, is referential transparency (tính minh bạch của tham chiếu) : i.e., since there is only a single definition for each variable in the program text, a variable’s value is independent of (phụ thuộc) its position in the program." {% endhint %} Do đó, thứ tự của các phép gán biến không thành vấn đề. ### 2.6 Theories **QF\_S** – strings. You may need this to simulate strings to catch bugs like SQL injection. . edu/wiki/Strings. {% hint style="success" %} * **QF\_UF** (Uninterpreted Functions): quantifier -free formulas whose satisfiability is to be decided modulo the empty theory. Each benchmark may introduce its own uninterpreted function and predicate symbols. * **QF\_IDL** (Integer Difference Logic): quantifier -free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to difference logic , i.e. x - y op c, where op is either equality or inequality and c is an integer constant. * **QF\_RDL** (Real Difference Logic): this division is like QF\_IDL , except that the background theory is real arithmetic. * **QF\_UFIDL** (Integer Difference Logic with Uninterpreted Functions): this division contains benchmarks in a logic which is similar to QF\_IDL , except that it also allows uninterpreted functions and predicates. * **QF\_LIA** (Linear Integer Arithmetic): quantifier -free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to contain only linear terms. * **QF\_LRA** (Linear Real Arithmetic): this division is like QF\_LIA , except that the background theory is real arithmetic. * **QF\_NIA** (Nonlinear Integer Arithmetic): quantifier -free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. There is no restriction to linear terms. * **QF\_UFLIA** (Linear Integer Arithmetic with Uninterpreted Functions): this division contains benchmarks in a logic which is similar to QF\_LIA , except that it also allows uninterpreted functions and predicates. * **QF\_UFLRA** (Linear Real Arithmetic with Uninterpreted Functions): this division is similar to QF\_LRA , except that it also allows uninterpreted functions and predicates. * **QF\_AX** (Arrays with Extensionality): quantifier -free formulas to be tested for satisfiability modulo a background theory of arrays which includes the extensionality axiom. * **QF\_AUFLIA** (Linear Integer Arithmetic with Uninterpreted Functions and Arrays): quantifier -free formulas to be tested for satisfiability modulo a background theory combining linear integer arithmetic , uninterpreted function and predicate symbols , and extensional arrays. * **QF\_BV** (Fixed -size Bit-vectors): quantifier -free formulas over bit vectors of fixed size. * **QF\_AUFBV** (Bit-vectors with Arrays and Uninterpreted Functions): quantifier -free formulas over bit vectors of fixed size, with arrays and uninterpreted functions and predicate symbols. * **AUFLIA+p** (Linear Integer Arithmetic with Uninterpreted Functions and Arrays , with patterns): quantified formulas to be tested for satisfiability modulo a background theory combining linear integer arithmetic , uninterpreted function and predicate symbols , and extensional arrays. Benchmarks include patterns for guiding instantiation mechanisms. * **AUFLIA -p** (Linear Integer Arithmetic with Uninterpreted Functions and Arrays , without patterns): formulas from AUFLIA+p once all patterns have been removed. * **AUFLIRA** (Arrays , Uninterpreted Functions , and Linear Arithmetic): quantifier formulas with arrays of reals indexed by integers (Array1), arrays of Array1 indexed by integers (Array2), and linear arithmetic over the integers and reals. * **UFNIA+p** (Uninterpreted Functions and Nonlinear Arithmetic , patterns included): quantifier formulas with uninterpreted functions and nonlinear integer arithmetic. * **AUFNIRA** (Arrays , Uninterpreted Functions , and Nonlinear Arithmetic): quantifier formulas with arrays of reals indexed by integers (Array1), arrays of Array1 indexed by integers (Array2), and nonlinear arithmetic over the integers and reals. {% endhint %} What is theory? * One can say that a SMT solver is a library of various (khác nhau) methods on top of a SAT solver. And sometimes, one theory/method can perform better for your problem than another. * You can first start without setting theory explicitly or setting QF\_ALL. But then you can experiment trying some of them. * And of course, SMT benchmarks for SMT solvers competition are divided by theories: . fr/zip. ### 2.7 Modulo `something` {% hint style="info" %} According to one dictionary, ”modulo” means ”correcting (sửa chữa) or adjusting (điều chỉnh) for something.” This is an appropriate (phù hợp) definition for its use in satisfiability modulo theories: First-order logic defines a notion of satisfiability (tính thỏa mãn) for arbitrary (bất kỳ) formulas. {% endhint %} ### 2.8 Division by 0 Họ không thể ném ngoại lệ, giống như CPU. Người ta đã quyết định tổng hợp hóa hoạt động của bộ phận, tức là làm cho nó tạo ra một đầu ra cho mỗi đầu vào. ``` Đa số mọi người thực hiện đã chọn như sau: (bvudiv x 0) = 11...1 Hợp lý khi định nghĩa: (bvurem x y) = x - (bvudiv x y) * y Khi y = 0 thì (bvurem x 0) = x ``` Nếu bạn muốn vô hiệu hóa phép chia cho số 0, bạn vẫn có thể thêm một ràng buộc ngăn số chia bằng 0. ### 2.9 Z3 specific The output is not guaranteed (đảm bảo) to be random. You can randomize it by: ```python import time ... s=Solver() set_param("smt.random_seed", int(time.time())) ``` Hoặc ngược lại, bạn có thể muốn sao chép kết quả của nó mỗi lần giống nhau (set seed bằng 1 số cố định): ```python set_param("smt.random_seed", 1234) ``` --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://viettaliii.gitbook.io/home/education/reverse-engineering/symbolic-analysis/sat-smt-by-example/basics/2.-smt-solvers.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.