From 52125f5f411a8783d9d90c50877b94c58585a30e Mon Sep 17 00:00:00 2001 From: German Nikolishin Date: Sun, 31 Mar 2024 02:13:47 +0100 Subject: [PATCH] partially resolve models --- crates/verifier/src/ast.rs | 48 ++++++++- crates/verifier/src/executor.rs | 86 +++++++++++++-- crates/verifier/src/lib.rs | 2 +- crates/verifier/src/tests.rs | 32 +++--- crates/verifier/src/transformer.rs | 162 ++++++++++++++++------------- 5 files changed, 223 insertions(+), 107 deletions(-) diff --git a/crates/verifier/src/ast.rs b/crates/verifier/src/ast.rs index a259901..8025960 100644 --- a/crates/verifier/src/ast.rs +++ b/crates/verifier/src/ast.rs @@ -1,4 +1,8 @@ +use std::rc::Rc; + +use folidity_diagnostics::Report; use folidity_semantics::{ + ast::Expression, GlobalSymbol, Span, SymbolInfo, @@ -11,16 +15,22 @@ use z3::{ }, Context, Solver, + Sort, +}; + +use crate::{ + executor::SymbolicExecutor, + transformer::transform_expr, }; /// A declaration in the code AST. -#[derive(Debug, Clone)] +#[derive(Debug)] pub struct Declaration<'ctx> { /// Info about the declaration pub decl_sym: GlobalSymbol, /// Parent of the declaration. pub parent: Option, /// Constraint block of the declaration. - pub block: ConstraintBlock<'ctx>, + pub constraints: Vec>, } /// A singular constraint. @@ -42,13 +52,41 @@ impl<'ctx> Constraint<'ctx> { pub fn sym_to_const<'a>(&self, ctx: &'a Context) -> Bool<'a> { Bool::new_const(ctx, self.binding_sym) } + + pub fn from_expr( + expr: &Expression, + ctx: &'ctx Context, + diagnostics: &mut Vec, + executor: &mut SymbolicExecutor<'ctx>, + ) -> Result, ()> { + let resolve_e = transform_expr(expr, &ctx, diagnostics, executor)?; + let Some(bool_expr) = resolve_e.element.as_bool() else { + diagnostics.push(Report::ver_error( + resolve_e.loc.clone(), + String::from("Expression must be boolean."), + )); + return Err(()); + }; + let (binding_const, n) = executor.create_constant(&Sort::bool(&ctx), &ctx); + + let binding_expr = binding_const + .as_bool() + .expect("must be bool") + .implies(&bool_expr); + + Ok(Constraint { + loc: resolve_e.loc.clone(), + binding_sym: n, + expr: binding_expr, + }) + } } /// Block of constraints of to be verified. -#[derive(Debug, Clone)] +#[derive(Debug)] pub struct ConstraintBlock<'ctx> { + pub context: Context, /// Solver which is scoped to the specific constraint block. - pub solver: Solver<'ctx>, /// List of constraints in the given block. pub constraints: Vec>, } @@ -57,7 +95,7 @@ impl<'ctx> ConstraintBlock<'ctx> { /// Translate context to the new solver. pub fn translate_to_solver<'a>(&self, solver: &Solver<'a>) -> Solver<'a> { let new_ctx = solver.get_context(); - self.solver.translate(new_ctx) + Solver::new(&self.context).translate(new_ctx) } /// Transform the list of ids of constraints into concrete boolean constants. diff --git a/crates/verifier/src/executor.rs b/crates/verifier/src/executor.rs index d7dcaa7..a3625a4 100644 --- a/crates/verifier/src/executor.rs +++ b/crates/verifier/src/executor.rs @@ -1,44 +1,108 @@ +use std::rc::Rc; + use folidity_diagnostics::Report; +use folidity_semantics::{ + ContractDefinition, + GlobalSymbol, + SymbolInfo, +}; use z3::{ - ast::Dynamic, + ast::{ + Ast, + Dynamic, + }, Context, Solver, Sort, }; -use crate::ast::Declaration; +use crate::{ + ast::{ + Constraint, + Declaration, + Z3Expression, + }, + transformer::transform_expr, + z3_cfg, +}; + +// -#[derive(Debug, Clone)] +#[derive(Debug)] pub struct SymbolicExecutor<'ctx> { /// Global solver of the executor. - solver: Solver<'ctx>, + /// + /// We encapsulate it as it can't be easily transferred between scopes. + context: Context, /// List of resolved declaration to verify. pub declarations: Vec>, + pub contexts: Vec, /// Symbol counter to track boolean constants across the program. pub symbol_counter: u32, pub diagnostics: Vec, } impl<'ctx> SymbolicExecutor<'ctx> { - pub fn new(context: &'ctx Context) -> Self { + pub fn new(context: Context) -> Self { Self { - solver: Solver::new(context), + context, + contexts: vec![], declarations: vec![], diagnostics: vec![], symbol_counter: 0, } } + pub fn parse_declarations(&mut self, contract: &ContractDefinition) -> Result<(), ()> { + let mut error = false; + let mut diagnostics = Vec::new(); + + for (i, m) in contract.models.iter().enumerate() { + let context = Context::new(&z3_cfg()); + let z3_exprs: Vec = m + .bounds + .iter() + .filter_map(|e| { + match transform_expr(e, &context, &mut diagnostics, self) { + Ok(c) => Some(c), + Err(_) => { + error = true; + None + } + } + }) + .collect(); + + // let decl = Declaration { + // decl_sym: GlobalSymbol::Model(SymbolInfo::new(m.loc.clone(), i)), + // parent: m.parent.clone(), + // constraints, + // }; + + // self.declarations.push(decl); + } + + if error { + return Err(()); + } + Ok(()) + } + /// Create a Z3 constant with the current symbol counter as a name while increasing /// the counter. - pub fn create_constant( + pub fn create_constant<'a>( &mut self, - sort: &Sort<'ctx>, - context: &'ctx Context, - ) -> (Dynamic<'ctx>, u32) { + sort: &Sort<'a>, + context: &'a Context, + ) -> (Dynamic<'a>, u32) { let id = self.symbol_counter; - let c = Dynamic::new_const(context, id, sort); + let c = Dynamic::new_const(&context, id, sort); self.symbol_counter += 1; (c, id) } + + /// Retrieve the context of the internal `solver`. + pub fn context(&self) -> &Context { + &self.context + } } diff --git a/crates/verifier/src/lib.rs b/crates/verifier/src/lib.rs index 111c6e0..5f72393 100644 --- a/crates/verifier/src/lib.rs +++ b/crates/verifier/src/lib.rs @@ -30,7 +30,7 @@ impl<'ctx> Runner for SymbolicExecutor<'ctx> { Self: std::marker::Sized, { let context = Context::new(&z3_cfg()); - let executor = SymbolicExecutor::new(&context); + let executor = SymbolicExecutor::new(context); Ok(()) } diff --git a/crates/verifier/src/tests.rs b/crates/verifier/src/tests.rs index 9a913d0..36e290d 100644 --- a/crates/verifier/src/tests.rs +++ b/crates/verifier/src/tests.rs @@ -14,10 +14,7 @@ use num_bigint::{ use num_traits::FromPrimitive; use z3::{ ast::{ - exists_const, - forall_const, Ast, - Bool, Int, Set, String as Z3String, @@ -55,8 +52,9 @@ fn mul_transform() { }); let context = Context::new(&z3_cfg()); - let mut executor = SymbolicExecutor::new(&context); - let z3_res = transform_expr(&mul, &context, &mut executor); + let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg())); + let mut diagnostics = vec![]; + let z3_res = transform_expr(&mul, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_e = z3_res.expect("Should be Ok"); @@ -76,8 +74,9 @@ fn var_transform() { }); let context = Context::new(&z3_cfg()); - let mut executor = SymbolicExecutor::new(&context); - let z3_res = transform_expr(&var, &context, &mut executor); + let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg())); + let mut diagnostics = vec![]; + let z3_res = transform_expr(&var, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_e = z3_res.expect("Should be Ok"); @@ -94,8 +93,9 @@ fn string_hex_transform() { }); let context = Context::new(&z3_cfg()); - let mut executor = SymbolicExecutor::new(&context); - let z3_res = transform_expr(&string, &context, &mut executor); + let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg())); + let mut diagnostics = vec![]; + let z3_res = transform_expr(&string, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_e = z3_res.expect("Should be Ok"); @@ -109,7 +109,7 @@ fn string_hex_transform() { element: hex::decode("AB").unwrap(), ty: TypeVariant::Int, }); - let z3_res = transform_expr(&hex, &context, &mut executor); + let z3_res = transform_expr(&hex, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_e = z3_res.expect("Should be Ok"); @@ -145,8 +145,9 @@ fn list_transform() { }); let context = Context::new(&z3_cfg()); - let mut executor = SymbolicExecutor::new(&context); - let z3_res = transform_expr(&list, &context, &mut executor); + let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg())); + let mut diagnostics = vec![]; + let z3_res = transform_expr(&list, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_e = z3_res.expect("Should be Ok"); @@ -233,11 +234,12 @@ fn in_transform() { }); let context = Context::new(&z3_cfg()); - let mut executor = SymbolicExecutor::new(&context); + let mut executor = SymbolicExecutor::new(Context::new(&z3_cfg())); + let mut diagnostics = vec![]; // verify that `30` is in the list. let solver = Solver::new(&context); - let z3_res = transform_expr(&in_true, &context, &mut executor); + let z3_res = transform_expr(&in_true, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_in_true = z3_res.expect("Ok"); solver.push(); @@ -248,7 +250,7 @@ fn in_transform() { solver.push(); // verify that `40` is not in the list. - let z3_res = transform_expr(&in_false, &context, &mut executor); + let z3_res = transform_expr(&in_false, &context, &mut diagnostics, &mut executor); assert!(z3_res.is_ok()); let z3_in_true = z3_res.expect("Ok"); solver.assert(&z3_in_true.element.as_bool().expect("Should be bool.").not()); diff --git a/crates/verifier/src/transformer.rs b/crates/verifier/src/transformer.rs index 7932566..7b12244 100644 --- a/crates/verifier/src/transformer.rs +++ b/crates/verifier/src/transformer.rs @@ -29,11 +29,12 @@ use crate::{ /// Transforms [`folidity_semantics::ast::Expression`] into [`crate::ast::Z3Expression`] /// in some given context [`z3::Context`]. -pub fn transform_expr<'ctx>( +pub fn transform_expr<'ctx, 'a>( expr: &Expression, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { +) -> Result, ()> { match expr { // literals Expression::Int(u) => Ok(int(&u.element, &u.loc, ctx)), @@ -54,20 +55,22 @@ pub fn transform_expr<'ctx>( | Expression::Less(_) | Expression::LessEq(_) | Expression::Greater(_) - | Expression::GreaterEq(_) => int_real_op(expr, ctx, executor), + | Expression::GreaterEq(_) => int_real_op(expr, ctx, diagnostics, executor), - Expression::Modulo(b) => modulo(&b.left, &b.right, &b.loc, ctx, executor), - Expression::Equal(b) => equality(&b.left, &b.right, &b.loc, ctx, executor), - Expression::NotEqual(b) => inequality(&b.left, &b.right, &b.loc, ctx, executor), - Expression::Not(u) => not(&u.element, &u.loc, ctx, executor), + Expression::Modulo(b) => modulo(&b.left, &b.right, &b.loc, ctx, diagnostics, executor), + Expression::Equal(b) => equality(&b.left, &b.right, &b.loc, ctx, diagnostics, executor), + Expression::NotEqual(b) => { + inequality(&b.left, &b.right, &b.loc, ctx, diagnostics, executor) + } + Expression::Not(u) => not(&u.element, &u.loc, ctx, diagnostics, executor), - Expression::Or(b) => or(&b.left, &b.right, &b.loc, ctx, executor), - Expression::And(b) => and(&b.left, &b.right, &b.loc, ctx, executor), + Expression::Or(b) => or(&b.left, &b.right, &b.loc, ctx, diagnostics, executor), + Expression::And(b) => and(&b.left, &b.right, &b.loc, ctx, diagnostics, executor), Expression::Variable(_) => variable(expr, ctx, executor), Expression::MemberAccess(_) => variable(expr, ctx, executor), - Expression::List(l) => list(&l.element, &l.loc, &l.ty, ctx, executor), - Expression::In(b) => in_(&b.left, &b.right, &b.loc, ctx, executor), + Expression::List(l) => list(&l.element, &l.loc, &l.ty, ctx, diagnostics, executor), + Expression::In(b) => in_(&b.left, &b.right, &b.loc, ctx, diagnostics, executor), Expression::FunctionCall(_) => { todo!("Verification of function calls is currently unsupported.") @@ -78,17 +81,18 @@ pub fn transform_expr<'ctx>( } } -fn in_<'ctx>( +fn in_<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let set = e2.element.as_set().ok_or_else(|| { - executor.diagnostics.push(Report::ver_error( + diagnostics.push(Report::ver_error( right.loc().clone(), String::from("Expression can not be coerces to a Z3 `Set`"), )); @@ -99,32 +103,33 @@ fn in_<'ctx>( Ok(Z3Expression::new(loc, &assertion)) } -fn list<'ctx>( +fn list<'ctx, 'a>( exprs: &[Expression], loc: &Span, ty: &TypeVariant, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { +) -> Result, ()> { let mut set = Set::empty(ctx, &type_to_sort(ty, ctx)); for e in exprs { - let z3_e = transform_expr(e, ctx, executor)?; + let z3_e = transform_expr(e, ctx, diagnostics, executor)?; set = set.add(&z3_e.element); } Ok(Z3Expression::new(loc, &set)) } -fn variable<'ctx>( +fn variable<'ctx, 'a>( e: &Expression, - ctx: &'ctx Context, + ctx: &'a Context, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { +) -> Result, ()> { let sort = type_to_sort(e.ty(), ctx); let res = executor.create_constant(&sort, ctx); Ok(Z3Expression::new(e.loc(), &res.0)) } -fn type_to_sort<'ctx>(ty: &TypeVariant, ctx: &'ctx Context) -> Sort<'ctx> { +fn type_to_sort<'ctx, 'a>(ty: &TypeVariant, ctx: &'a Context) -> Sort<'a> { match ty { TypeVariant::Int | TypeVariant::Uint | TypeVariant::Char | TypeVariant::Enum(_) => { Sort::int(ctx) @@ -150,11 +155,12 @@ fn type_to_sort<'ctx>(ty: &TypeVariant, ctx: &'ctx Context) -> Sort<'ctx> { } } -fn int_real_op<'ctx>( +fn int_real_op<'ctx, 'a>( e: &Expression, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { +) -> Result, ()> { let (Expression::Multiply(b) | Expression::Divide(b) | Expression::Add(b) @@ -166,8 +172,8 @@ fn int_real_op<'ctx>( else { unreachable!("Only [*, /, +, -, >, <, ≥, ≤] ops are allowed to be passed."); }; - let e1 = transform_expr(&b.left, ctx, executor)?; - let e2 = transform_expr(&b.right, ctx, executor)?; + let e1 = transform_expr(&b.left, ctx, diagnostics, executor)?; + let e2 = transform_expr(&b.right, ctx, diagnostics, executor)?; let mut reports = Vec::new(); let int1 = to_z3_int(&e1, &mut reports); let int2 = to_z3_int(&e2, &mut reports); @@ -201,7 +207,7 @@ fn int_real_op<'ctx>( } } _ => { - executor.diagnostics.push(Report::ver_error_with_extra( + diagnostics.push(Report::ver_error_with_extra( b.loc.clone(), String::from("Can not apply arithmetic operation on these data ."), reports, @@ -215,15 +221,16 @@ fn int_real_op<'ctx>( }) } -fn modulo<'ctx>( +fn modulo<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let mut reports = Vec::new(); let int1 = to_z3_int(&e1, &mut reports); @@ -234,7 +241,7 @@ fn modulo<'ctx>( Ok(Z3Expression::new(loc, &res)) } _ => { - executor.diagnostics.push(Report::ver_error_with_extra( + diagnostics.push(Report::ver_error_with_extra( loc.clone(), String::from("Can not perform modulo operation."), reports, @@ -244,18 +251,19 @@ fn modulo<'ctx>( } } -fn equality<'ctx>( +fn equality<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let res = e1.element._safe_eq(&e2.element).map_err(|_| { - executor.diagnostics.push(Report::ver_error( + diagnostics.push(Report::ver_error( loc.clone(), String::from("Sort mismatch."), )) @@ -264,43 +272,46 @@ fn equality<'ctx>( Ok(Z3Expression::new(loc, &res)) } -fn inequality<'ctx>( +fn inequality<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let res = Dynamic::distinct(ctx, &[&e1.element, &e2.element]); Ok(Z3Expression::new(loc, &res)) } -fn not<'ctx>( +fn not<'ctx, 'a>( e: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let v = transform_expr(e, ctx, executor)?; +) -> Result, ()> { + let v = transform_expr(e, ctx, diagnostics, executor)?; - let bool_v = to_z3_bool(&v, &mut executor.diagnostics)?; + let bool_v = to_z3_bool(&v, diagnostics)?; Ok(Z3Expression::new(loc, &bool_v)) } -fn or<'ctx>( +fn or<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let mut reports = Vec::new(); let int1 = to_z3_bool(&e1, &mut reports); @@ -311,7 +322,7 @@ fn or<'ctx>( Ok(Z3Expression::new(loc, &res)) } _ => { - executor.diagnostics.push(Report::ver_error_with_extra( + diagnostics.push(Report::ver_error_with_extra( loc.clone(), String::from("Can not perform boolean OR."), reports, @@ -321,15 +332,16 @@ fn or<'ctx>( } } -fn and<'ctx>( +fn and<'ctx, 'a>( left: &Expression, right: &Expression, loc: &Span, - ctx: &'ctx Context, + ctx: &'a Context, + diagnostics: &mut Vec, executor: &mut SymbolicExecutor<'ctx>, -) -> Result, ()> { - let e1 = transform_expr(left, ctx, executor)?; - let e2 = transform_expr(right, ctx, executor)?; +) -> Result, ()> { + let e1 = transform_expr(left, ctx, diagnostics, executor)?; + let e2 = transform_expr(right, ctx, diagnostics, executor)?; let mut reports = Vec::new(); let int1 = to_z3_bool(&e1, &mut reports); @@ -340,7 +352,7 @@ fn and<'ctx>( Ok(Z3Expression::new(loc, &res)) } _ => { - executor.diagnostics.push(Report::ver_error_with_extra( + diagnostics.push(Report::ver_error_with_extra( loc.clone(), String::from("Can not perform boolean AND."), reports, @@ -350,32 +362,32 @@ fn and<'ctx>( } } -fn int<'ctx>(value: &BigInt, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn int<'ctx, 'a>(value: &BigInt, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Int::from_big_int(ctx, value); Z3Expression::new(loc, &c) } -fn real<'ctx>(value: &BigRational, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn real<'ctx, 'a>(value: &BigRational, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Real::from_big_rational(ctx, value); Z3Expression::new(loc, &c) } -fn bool<'ctx>(value: bool, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn bool<'ctx, 'a>(value: bool, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Bool::from_bool(ctx, value); Z3Expression::new(loc, &c) } -fn string<'ctx>(value: &str, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn string<'ctx, 'a>(value: &str, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Z3String::from_str(ctx, value).unwrap_or(Z3String::fresh_const(ctx, "")); Z3Expression::new(loc, &c) } -fn char<'ctx>(value: char, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn char<'ctx, 'a>(value: char, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Int::from_u64(ctx, value as u64); Z3Expression::new(loc, &c) } -fn enum_<'ctx>(value: usize, loc: &Span, ctx: &'ctx Context) -> Z3Expression<'ctx> { +fn enum_<'ctx, 'a>(value: usize, loc: &Span, ctx: &'a Context) -> Z3Expression<'a> { let c = Int::from_u64(ctx, value as u64); Z3Expression::new(loc, &c) } @@ -429,10 +441,10 @@ fn to_z3_string<'ctx>( } /// Create a boolean constant and returns its id as `u32` -pub fn create_constraint_const<'ctx>( - ctx: &'ctx Context, +pub fn create_constraint_const<'ctx, 'a>( + ctx: &'a Context, executor: &mut SymbolicExecutor<'ctx>, -) -> (Bool<'ctx>, u32) { +) -> (Bool<'a>, u32) { let val = executor.create_constant(&Sort::bool(ctx), ctx); (val.0.as_bool().unwrap(), val.1) }