z3

GitHub - Z3Prover/z3: The Z3 Theorem Prover

• z3.rs

tpp2011/ucd.smt2 at master · msakai/tpp2011 · GitHub

Array

Can’t choose a symbolic array index? · Issue #70 · prove-rs/z3.rs · GitHub
z3test/array.smt2 at master · Z3Prover/z3test · GitHub

let A = Array::new_const(&ctx, "A", &Sort::int(&ctx), &Sort::int(&ctx));
 
A.store(&Dynamic::from_ast(&Int::from_u64(&ctx, 0)),
    &Dynamic::from_ast(&x.sub(&[&y])),
);

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (< x z))
(assert (< y z))
(assert (< z 5))
(assert (not (= x y)))
(maximize x)
(maximize y)
(check-sat)
(get-model)
(get-objectives)
 

forall

MathSAT SMT-LIBv2 Examples

z3::ast::forall_const - Rust

SMT2 format

Programming Z3

参考文献

• https://sat-smt.codes/SAT_SMT_by_example.pdf
  • 大量に例が載っている神みたいなPDF