Function z3::ast::forall_const

pub fn forall_const<'ctx>(
    ctx: &'ctx Context, 
    bounds: &[&Dynamic<'ctx>], 
    patterns: &[&Pattern<'ctx>], 
    body: &Dynamic<'ctx>
) -> Dynamic<'ctx>

Create a universal quantifier.

Examples

let f = FuncDecl::new(&ctx, "f", &[&Sort::int(&ctx)], &Sort::int(&ctx));

let x = ast::Int::new_const(&ctx, "x");
let f_x: ast::Int = f.apply(&[&x.clone().into()]).try_into().unwrap();
let f_x_pattern: Pattern = Pattern::new(&ctx, &[ &f_x.clone().into() ]);
let forall: ast::Bool = ast::forall_const(
    &ctx,
    &[&x.clone().into()],
    &[&f_x_pattern],
    &x._eq(&f_x).into()
).try_into().unwrap();
solver.assert(&forall);

assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model();

let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3).into()])]).try_into().unwrap();
assert_eq!(3, model.eval(&f_f_3).unwrap().as_u64().unwrap());