Hỗ trợ định lượng Z3

Question

Tôi cần một định lý lý thuyết cho một số vấn đề số học tuyến tính đơn giản. Tuy nhiên, tôi không thể có được Z3 để làm việc ngay cả trên các vấn đề đơn giản. Tôi biết rằng nó là không đầy đủ, tuy nhiên nó sẽ có thể xử lý các ví dụ đơn giản này:

(assert (forall ((t Int)) (= t 5))) 
(check-sat) 

Tôi không chắc chắn nếu tôi đang nhìn cái gì đó, nhưng điều này nên được tầm thường để bác bỏ. Tôi thậm chí đã thử ví dụ đơn giản này:

(assert (forall ((t Bool)) (= t true))) 
(check-sat) 

Điều đó phải được giải quyết bằng cách thực hiện tìm kiếm toàn diện, vì khởi động chỉ chứa hai giá trị.

Trong cả hai trường hợp, câu trả lời z3 không rõ. Tôi muốn biết nếu tôi đang làm một cái gì đó sai ở đây hoặc nếu không nếu bạn có thể giới thiệu một định lý prover cho các loại công thức.

Answer 1

Để xử lý loại định lượng này, bạn nên sử dụng mô-đun loại bỏ định lượng có sẵn trong Z3. Dưới đây là một ví dụ về cách sử dụng nó (thử trực tuyến tại http://rise4fun.com/Z3/3C3):

(assert (forall ((t Int)) (= t 5))) 
(check-sat-using (then qe smt)) 

(reset) 

(assert (forall ((t Bool)) (= t true))) 
(check-sat-using (then qe smt)) 

Lệnh check-sat-using cho phép chúng ta xác định một chiến lược để giải quyết vấn đề. Trong ví dụ trên, tôi chỉ sử dụng qe (loại bỏ định lượng) và sau đó gọi một bộ giải quyết SMT mục đích chung. Lưu ý rằng, đối với các ví dụ này, qe là đủ.

Dưới đây là một ví dụ phức tạp hơn, nơi mà chúng tôi thực sự cần phải kết hợp qe và smt (thử trực tuyến tại địa chỉ: http://rise4fun.com/Z3/l3Rl)

(declare-const a Int) 
(declare-const b Int) 
(assert (forall ((t Int)) (=> (<= t a) (< t b)))) 
(check-sat-using (then qe smt)) 
(get-model) 

EDIT Dưới đây là ví dụ tương tự bằng cách sử dụng ++ API C/C:

void tactic_qe() { 
    std::cout << "tactic example using quantifier elimination\n"; 
    context c; 

    // Create a solver using "qe" and "smt" tactics 
    solver s = 
     (tactic(c, "qe") & 
     tactic(c, "smt")).mk_solver(); 

    expr a = c.int_const("a"); 
    expr b = c.int_const("b"); 
    expr x = c.int_const("x"); 
    expr f = implies(x <= a, x < b); 

    // We have to use the C API directly for creating quantified formulas. 
    Z3_app vars[] = {(Z3_app) x}; 
    expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars, 
              0, 0, // no pattern 
              f)); 
    std::cout << qf << "\n"; 

    s.add(qf); 
    std::cout << s.check() << "\n"; 
    std::cout << s.get_model() << "\n"; 
}