z3_constraint!() { /* proc-macro */ }Expand description
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)));