Crate easyz3
Source - z3_constraint
- add constraint on int formula:
z3constraint!(a * 94 + b * 34 == 8400);
=> solver.assert(&Int::_eq(&Int::add(&ctx, &[&Int::mul(&ctx, &[&a, &Int::from_i64(&ctx, 94)]), &Int::mul(&ctx, &[&b, &Int::from_i64(&ctx, 34)])]), &Int::from_i64(&ctx, 8400)));
- z3_constraint_u8
- z3_constraint_u16
- z3_constraint_u32
- z3_constraint_u64
- z3_distinct
- add constraint on int formula:
z3constraint!(a * 94 + b * 34 == 8400);
=> solver.assert(&Int::_eq(&Int::add(&ctx, &[&Int::mul(&ctx, &[&a, &Int::from_i64(&ctx, 94)]), &Int::mul(&ctx, &[&b, &Int::from_i64(&ctx, 34)])]), &Int::from_i64(&ctx, 8400)));
- z3_formula
- formula about z3 ints:
let eq1 = z3_formula!(a * 94 + b * 34 == 8400);
=> let eq1 = Int::_eq(&Int::add(&ctx, &[&Int::mul(&ctx, &[&a, &Int::from_i64(&ctx, 94)]), &Int::mul(&ctx, &[&b, &Int::from_i64(&ctx, 34)])]), &Int::from_i64(&ctx, 8400));
- z3_formula_u8
- z3_formula_u16
- z3_formula_u32
- z3_formula_u64
- z3_init
- init z3 in the most common way:
z3_init!()
=> let config = Config::new();
let ctx = Context::new(&config);
let solver = Solver::new(&ctx);
- z3_init_u8
- z3_init_u16
- z3_init_u32
- z3_init_u64
- z3_solve
- usage:
if let Some((a,b)) = z3solve!(a,b) {
println(“Solution: a:{} b:{}”,a,b);
} else{
println!(“unsat :-(”);
}
- z3_solve_u8
- z3_solve_u16
- z3_solve_u32
- z3_solve_u64
- z3_var
- declare int variable
z3var!(a);
=> let a = ast::Int::new_const(&ctx, “a”);
- z3_var_u8
- declare bv variables
- z3_var_u16
- z3_var_u32
- z3_var_u64