Function z3::ast::exists_const [−][src]
pub fn exists_const<'ctx>(
ctx: &'ctx Context,
bounds: &[&dyn Ast<'ctx>],
patterns: &[&Pattern<'ctx>],
body: &Bool<'ctx>
) -> Bool<'ctx>
Expand description
Create an existential 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]).try_into().unwrap();
let f_x_pattern: Pattern = Pattern::new(&ctx, &[ &f_x ]);
let exists: ast::Bool = ast::exists_const(
&ctx,
&[&x],
&[&f_x_pattern],
&x._eq(&f_x).not()
).try_into().unwrap();
solver.assert(&exists.not());
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();;
let f_f_3: ast::Int = f.apply(&[&f.apply(&[&ast::Int::from_u64(&ctx, 3)])]).try_into().unwrap();
assert_eq!(3, model.eval(&f_f_3, true).unwrap().as_u64().unwrap());