cvc3 - Trực tuyến trên đám mây

CHƯƠNG TRÌNH:

TÊN

cvc3 - câu châm ngôn về định lý SMT tự động

SYNOPSIS

cvc3 [tùy chọn] ... [tên tập tin]

MÔ TẢ

HVAC3 là một trình kiểm tra tính hợp lệ tự động cho logic bậc nhất được sắp xếp nhiều (đã đánh máy) với
các lý thuyết tích hợp, bao gồm một số hỗ trợ cho các bộ định lượng, các chức năng từng phần và
các kiểu phụ vị ngữ. Các lý thuyết được xây dựng hiện tại là các lý thuyết về

· Bình đẳng về hàm và ký hiệu vị ngữ miễn phí (hay còn gọi là không được thông dịch),

· Số học tuyến tính thực và số nguyên (với một số hỗ trợ cho số học phi tuyến tính),

· Vectơ bit,

· Mảng,

· Bộ giá trị,

· Hồ sơ,

· Kiểu dữ liệu quy nạp do người dùng xác định.

CVC3 hoạt động trên các tệp trong CVC Trình bày Đầu vào Ngôn ngữ hoặc là SMTLIB đầu vào
ngôn ngữ. Nếu không có tệp đầu vào nào được đưa ra trên dòng lệnh, CVC3 sẽ đọc đầu vào chuẩn.

LỰA CHỌN

Dưới đây chỉ đưa ra một số tùy chọn được sử dụng thường xuyên nhất. Để biết thêm chi tiết, hãy xem
Trợ giúp tích hợp sẵn của CVC3 (cvc3 -Cứu giúp) hoặc trang web CVC3.

-Cứu giúp]
Liệt kê tất cả các tùy chọn để kiểm soát CVC3. Tùy chọn boolean được đánh dấu (B). Họ
được kích hoạt bằng cách thêm tiền tố + và bị vô hiệu hóa bằng cách thêm tiền tố -. Trong sự giúp đỡ
đầu ra, hiện hành cài đặt được đưa ra. Ví dụ, danh sách đầu ra

(b)-Chế độ tương tác tương tác

Cho biết rằng chế độ tương tác đã bị tắt. để bật chế độ tương tác,
tùy chọn + tương tác do đó được sử dụng. Các tùy chọn khác được đánh dấu (S) cho chuỗi
đối số, hoặc (I) cho các đối số nguyên.

-phiên bản
In phiên bản CVC3 và thoát.

-lang (trình bày|smtlib|nội bộ) Chọn ngôn ngữ nhập được sử dụng. Mặc định là
trình bày.

+ int [eractive]
Bật chế độ tương tác. Các lệnh được đọc từ đầu vào chuẩn và được xử lý
ngay lập tức.

+ số liệu thống kê In thống kê thời gian chạy.

-hết giờ t
Tự động chấm dứt CVC3 sau t giây.

Sử dụng cvc3 trực tuyến bằng các dịch vụ onworks.net