Examples

[cryslith]

It would be great if https://docs.rs/z3 had some top-level documentation with full usage examples for the crate, or linked to useful examples elsewhere. As it is, it's a bit intimidating to look at the whole crate without knowing where to start.

[sameer]

That's a fair call-out. The tests provide some examples, though a lot of it assumes you have general background with SMT solvers and Z3.

Most of the maintainers including myself are strapped for time, but will try to expand on the docs.

If this is something you'd be interested in helping out with I'm happy to review any PRs :slightly_smiling_face:

[jakeisnt]

I've found a couple of good examples here; I've opened a quick PR to fix one of the examples after updating the z3 crate for that repository but am having some trouble with the other (trio).

If anyone has some time to help fix the example and/or provide a brief explanation of what could be wrong, I'd really appreciate it!

[aquarial]

Here's an example solving a DIMACS formatted problem. It's the simplest useful thing to do with z3.rs. Clean it up a bit, and I think would be great for the README.

Answers some of the questions I had when I first looked at the library, and puts the doc.rs into a context.

Shows how to:

• create config/context/optimize structs
• create Bool AST
• store variables and query from the model

if args[1].clone() == String::from("DIMACS") {
    let instr = std::fs::read_to_string(args[2].clone()).unwrap();

    let mut all_vars = HashSet::<u32>::new();

    let config = z3::Config::new();
    let context = z3::Context::new(&config);
    let opt = z3::Optimize::new(&context);

    // parse DIMACS
    for strline in instr.trim().split("\n") {
        if strline.chars().nth(0) == Some('p') {
            continue;
        }

        let mut vals = Vec::<z3::ast::Bool>::new();
        strline.trim().split(" ").filter(|v| v != &"0").for_each(|v| {
            let v: i64 = v.parse().unwrap();
            all_vars.insert(v.abs() as u32);

            let symb = z3::ast::Bool::new_const(&context, v.abs() as u32);
            vals.push(if v > 0 { symb } else { symb.not() });
        });
        let refvals: Vec<&z3::ast::Bool> = vals.iter().collect();
        opt.assert(&z3::ast::Bool::or(&context, &refvals));
    }

    // solve puzzle
    let result: z3::SatResult = opt.check(&[]);
    let model: z3::Model = opt.get_model().unwrap();

    // query+output values
    println!("s {:?}", result);
    print!("v ");
    for var in all_vars.iter() {
        let symb = z3::ast::Bool::new_const(&context, *var);
        if let Some(res) = model.eval(&symb, true) {
            if res.as_bool() == Some(true) {
                print!("{} ", var);
            } else {
                print!("-{} ", var);
            }
        }
    }
    println!("0");
}

[detrin]

I would be awesome to have some kind of minimal example for SAT in z3 rust binding, such as here in python http://www.cs.toronto.edu/~victorn/tutorials/z3_SAT_2019/index.html

I have created as a fun project pentomino solver with SAT https://github.com/detrin/rust-sat-polyomino I am using https://github.com/jix/varisat solver but it is not currently developed, single-threaded and doesn't support multiple results outputting.