#smt #z3 #language #solver

bin+lib smt-lang

Sat Modulo Theory Language

19 releases (5 breaking)

0.7.5 Feb 17, 2023
0.6.3 Dec 12, 2022
0.6.2 Nov 28, 2022

#231 in Math

Download history 71/week @ 2022-11-22 33/week @ 2022-11-29 30/week @ 2022-12-06 26/week @ 2022-12-13 1/week @ 2022-12-20 1/week @ 2022-12-27 7/week @ 2023-01-10 2/week @ 2023-01-17 4/week @ 2023-01-24 85/week @ 2023-01-31 46/week @ 2023-02-07 74/week @ 2023-02-14 22/week @ 2023-02-21 2/week @ 2023-02-28

98 downloads per month

LGPL-3.0-only

250KB
6.5K SLoC

Install

  1. Install Rust: Rust
  2. Install clang:
     xxx@XXX:~$ sudo apt install clang
    
  3. Install SMT-Language:
     xxx@XXX:~$ cargo install smt-lang
    

Run SMT-language

xxx@XXX:~$ smt-lang --file problem_file.sl

Example

Problem

let b: Bool
let i: 1..100
let r: Real

constraint C1 = (
    i >= 10
)
constraint C2 = (
    r <= 20.0 and b
)

Solve

xxx@XXX:~$ smt-lang --file example.sl

Solution

let b: Bool = true
let i: 1..100 = 10
let r: Real = 20

Options

Verbose

  • --verbose 0 : display nothing except the result
  • --verbose 1 : display analysis result
  • --verbose 2 : display loaded problem
  • --verbose 3 : display SMT problem and SMT model if a solution is found

Syntax

Dependencies

~30MB
~628K SLoC