diff --git a/src/driver/commands/get_pre_models.rs b/src/driver/commands/get_pre_models.rs new file mode 100644 index 00000000..3a663875 --- /dev/null +++ b/src/driver/commands/get_pre_models.rs @@ -0,0 +1,215 @@ +use std::{ops::DerefMut, process::ExitCode, sync::Arc}; + +use crate::{ + ast::{BinOpKind, Direction, ExprBuilder, FileId, Span, TyKind}, + driver::{ + commands::{mk_cli_server, print_timings, verify::VerifyCommand}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, + error::{finalize_caesar_result, CaesarError}, + front::parse_and_tycheck, + item::Item, + quant_proof::BoolVcProveTask, + smt_proof::{run_smt_check_sat, set_global_z3_params}, + }, + resource_limits::{await_with_resource_limits, LimitsRef}, + servers::{Server, SharedServer}, +}; +use z3::SatResult; + +pub async fn run_nontrivial_model_command(options: VerifyCommand) -> ExitCode { + let (user_files, server) = match mk_cli_server(&options.input_options) { + Ok(value) => value, + Err(value) => return value, + }; + let options = Arc::new(options); + let nontrivial_models_result = nontrivial_model_files(&options, &server, user_files).await; + + if options.debug_options.timing { + print_timings(); + } + + finalize_caesar_result(server, &options.rlimit_options, nontrivial_models_result) +} + +/// This is just like verify_files() +pub async fn nontrivial_model_files( + options: &Arc, + server: &SharedServer, + user_files: Vec, +) -> Result { + let handle = |limits_ref: LimitsRef| { + let options = options.clone(); + let server = server.clone(); + tokio::task::spawn_blocking(move || { + // execute the verifier with a larger stack size of 50MB. the + // default stack size might be quite small and we need to do quite a + // lot of recursion. + let stack_size = 50 * 1024 * 1024; + stacker::maybe_grow(stack_size, stack_size, move || { + let mut server = server.lock().unwrap(); + nontrivial_model_files_main(&options, limits_ref, server.deref_mut(), &user_files) + }) + }) + }; + // Unpacking lots of Results with `.await??` :-) + await_with_resource_limits( + Some(options.rlimit_options.timeout()), + Some(options.rlimit_options.mem_limit()), + handle, + ) + .await?? +} + +fn nontrivial_model_files_main( + options: &VerifyCommand, + limits_ref: LimitsRef, + server: &mut dyn Server, + user_files: &[FileId], +) -> Result { + let (mut module, mut tcx) = parse_and_tycheck( + &options.input_options, + &options.debug_options, + server, + user_files, + )?; + + // Register all relevant source units with the server + module.register_with_server(server)?; + + // explain high-level HeyVL if requested + if options.lsp_options.explain_vc { + module.explain_high_level_vc(&tcx, &limits_ref, server)?; + } + + // Desugar encodings from source units. + module.apply_encodings(&mut tcx, server)?; + + if options.debug_options.print_core_procs { + println!("HeyVL get nontrivial model task with generated procs:"); + println!("{module}"); + } + + // generate dependency graph to determine which declarations are needed for + // the SMT translation later + let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; + + // translate program to relevant preexpectation conditions + let mut verify_units: Vec> = module + .items + .into_iter() + .flat_map(|item| { + item.flat_map(|unit| CoreHeyVLTask::from_proc_pre_model(unit, &mut depgraph)) + }) + .collect(); + + if options.debug_options.z3_trace && verify_units.len() > 1 { + tracing::warn!("Z3 tracing is enabled with multiple units. Intermediate tracing results will be overwritten."); + } + // set requested global z3 options + set_global_z3_params(options, &limits_ref); + + let mut num_sat: usize = 0; + let mut num_unsat: usize = 0; + + for verify_unit in &mut verify_units { + limits_ref.check_limits()?; + + let (name, mut verify_unit) = verify_unit.enter_with_name(); + + // Set the current unit as ongoing + server.set_ongoing_unit(name)?; + + // no slicing + let mut new_options = VerifyCommand::default(); + new_options.slice_options.no_slice_error = true; + + let (vc_expr, _slice_vars) = lower_core_heyvl_task( + &mut tcx, + name, + &new_options, + &limits_ref, + server, + &mut verify_unit, + )?; + + // Lowering the quantitative task to a Boolean one. + let mut quant_task = vc_expr; + + // Unfolding (applies substitutions) + quant_task.unfold(options, &limits_ref, &tcx)?; + + quant_task.trace_expr_stats(); + + // Turn quantitative formula into a Boolean one + let builder = ExprBuilder::new(Span::dummy_span()); + let expr = quant_task.expr.clone(); + + // Construct the condition based on quantifier direction + let res = match quant_task.direction { + Direction::Up => { + // For coprocs, check if expr < top + let top = builder.top_lit(quant_task.expr.ty.as_ref().unwrap()); + builder.binary(BinOpKind::Lt, Some(TyKind::Bool), expr, top) + } + Direction::Down => { + // For procs, check if expr > bot + let bot = builder.bot_lit(quant_task.expr.ty.as_ref().unwrap()); + builder.binary(BinOpKind::Gt, Some(TyKind::Bool), expr, bot) + } + }; + + // Create a Boolean verification task with the comparison + let mut bool_task = BoolVcProveTask { + quant_vc: quant_task, + vc: res, + }; + + // Optimizations + if !options.opt_options.no_boolify || options.opt_options.opt_rel { + bool_task.remove_parens(); + } + if !options.opt_options.no_boolify { + bool_task.opt_boolify(); + } + if options.opt_options.opt_rel { + bool_task.opt_relational(); + } + + if options.debug_options.print_theorem { + bool_task.print_theorem(name); + } + + // Running the SMT check sat task: translating to Z3, running the solver. + // This also handles printing the result + let sat_result = run_smt_check_sat( + &options, + &limits_ref, + &tcx, + &depgraph, + &name, + bool_task, + server, + )?; + + // Handle reasons to stop the verifier. + match sat_result { + SatResult::Unknown => return Err(CaesarError::Interrupted), + _ => {} + } + + // Increment counters. + match sat_result { + SatResult::Sat => num_sat += 1, + SatResult::Unsat | SatResult::Unknown => num_unsat += 1, + } + } + + if !options.lsp_options.language_server { + println!(); + println!( + "Found models for {num_sat} (co)procedures, No models for {num_unsat} (co)procedures." + ); + } + + Ok(num_unsat == 0) +} diff --git a/src/driver/commands/mod.rs b/src/driver/commands/mod.rs index b09d0318..730ded53 100644 --- a/src/driver/commands/mod.rs +++ b/src/driver/commands/mod.rs @@ -1,5 +1,6 @@ //! (CLI) command and option declarations to run Caesar with. +pub mod get_pre_models; pub mod model_check; pub mod options; pub mod refinement; @@ -19,6 +20,7 @@ use clap::{crate_description, Args, CommandFactory, Parser, Subcommand}; use crate::{ ast::FileId, driver::commands::{ + get_pre_models::run_nontrivial_model_command, model_check::{run_model_checking_command, ModelCheckCommand}, options::{DebugOptions, InputOptions}, refinement::run_verify_entailment_command, @@ -65,6 +67,7 @@ impl CaesarCli { CaesarCommand::Mc(options) => run_model_checking_command(options), CaesarCommand::Lsp(options) => run_lsp_command(options).await, CaesarCommand::ShellCompletions(options) => run_shell_completions_command(options), + CaesarCommand::GetPreModels(options) => run_nontrivial_model_command(options).await, CaesarCommand::Other(_) => unreachable!(), } } @@ -98,6 +101,8 @@ pub enum CaesarCommand { Lsp(VerifyCommand), /// Generate shell completions for the Caesar binary. ShellCompletions(ShellCompletionsCommand), + /// Compute a non-trivial model for the preconditions of each (co)proc. + GetPreModels(VerifyCommand), /// This is to support the default `verify` command. #[command(external_subcommand)] #[command(hide(true))] @@ -112,6 +117,7 @@ impl CaesarCommand { CaesarCommand::Lsp(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Mc(mc_options) => Some(&mc_options.debug_options), CaesarCommand::ShellCompletions(_) => None, + CaesarCommand::GetPreModels(verify_options) => Some(&verify_options.debug_options), CaesarCommand::Other(_vec) => unreachable!(), } } diff --git a/src/driver/commands/refinement.rs b/src/driver/commands/refinement.rs index 3f5c285e..48c9c913 100644 --- a/src/driver/commands/refinement.rs +++ b/src/driver/commands/refinement.rs @@ -17,7 +17,7 @@ use crate::{ }, driver::{ commands::{mk_cli_server, print_timings, verify::VerifyCommand}, - core_verify::{lower_core_verify_task, CoreVerifyTask}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, error::{finalize_caesar_result, CaesarError}, front::{parse_and_tycheck, SourceUnit}, item::Item, @@ -121,13 +121,13 @@ async fn verify_entailment( }; let mut first_verify_unit = first - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph)) + .flat_map(|u| CoreHeyVLTask::from_proc_verify(u, &mut depgraph)) .unwrap(); let mut second_verify_unit = second - .flat_map(|u| CoreVerifyTask::from_source_unit(u, &mut depgraph)) + .flat_map(|u| CoreHeyVLTask::from_proc_verify(u, &mut depgraph)) .unwrap(); - let (first_vc, first_slice_stmts) = lower_core_verify_task( + let (first_vc, first_slice_stmts) = lower_core_heyvl_task( &mut tcx, &first_name, options, @@ -135,7 +135,7 @@ async fn verify_entailment( server, &mut first_verify_unit.enter_mut(), )?; - let (second_vc, second_slice_stmts) = lower_core_verify_task( + let (second_vc, second_slice_stmts) = lower_core_heyvl_task( &mut tcx, &first_name, options, diff --git a/src/driver/commands/verify.rs b/src/driver/commands/verify.rs index 4fcf54e7..c8dfeef9 100644 --- a/src/driver/commands/verify.rs +++ b/src/driver/commands/verify.rs @@ -15,7 +15,7 @@ use crate::{ }, print_timings, }, - core_verify::{lower_core_verify_task, CoreVerifyTask}, + core_heyvl::{lower_core_heyvl_task, CoreHeyVLTask}, error::{finalize_caesar_result, CaesarError}, front::parse_and_tycheck, item::Item, @@ -211,11 +211,11 @@ fn verify_files_main( // the SMT translation later let mut depgraph = module.generate_depgraph(&options.opt_options.function_encoding)?; - let mut verify_units: Vec> = module + let mut verify_units: Vec> = module .items .into_iter() .flat_map(|item| { - item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph)) + item.flat_map(|unit| CoreHeyVLTask::from_proc_verify(unit, &mut depgraph)) }) .collect(); @@ -240,7 +240,7 @@ fn verify_files_main( // Lowering the core verify task to a quantitative prove task: applying // spec call desugaring, preparing slicing, and verification condition // generation. - let (vc_expr, slice_vars) = lower_core_verify_task( + let (vc_expr, slice_vars) = lower_core_heyvl_task( &mut tcx, name, options, diff --git a/src/driver/core_verify.rs b/src/driver/core_heyvl.rs similarity index 76% rename from src/driver/core_verify.rs rename to src/driver/core_heyvl.rs index 16a7219e..78bad721 100644 --- a/src/driver/core_verify.rs +++ b/src/driver/core_heyvl.rs @@ -21,7 +21,7 @@ use crate::{ }, pretty::{Doc, SimplePretty}, procs::{ - proc_verify::{encode_proc_verify, to_direction_lower_bounds}, + proc_verify::{encode_preexpectation, encode_proc_verify, to_direction_lower_bounds}, SpecCall, }, resource_limits::LimitsRef, @@ -39,13 +39,13 @@ use tracing::instrument; /// Lower a core verification task into a quantitative vc prove task: apply /// desugaring for spec calls, preparing slicing, and verification condition /// generation. -pub fn lower_core_verify_task( +pub fn lower_core_heyvl_task( tcx: &mut TyCtx, name: &SourceUnitName, options: &VerifyCommand, limits_ref: &LimitsRef, server: &mut dyn Server, - task: &mut CoreVerifyTask, + task: &mut CoreHeyVLTask, ) -> Result<(QuantVcProveTask, SliceStmts), CaesarError> { // 1. Desugaring task.desugar_spec_calls(tcx, name.to_string())?; @@ -66,33 +66,25 @@ pub fn lower_core_verify_task( /// A block of HeyVL statements to be verified with a certain [`Direction`]. #[derive(Debug, Clone)] -pub struct CoreVerifyTask { +pub struct CoreHeyVLTask { pub deps: Dependencies, pub direction: Direction, pub block: Block, } -impl CoreVerifyTask { - /// Convert this source unit into a [`CoreVerifyTask`]. Some declarations, +impl CoreHeyVLTask { + /// Convert proc_verify into a [`CoreHeyVLTask`]. Some declarations, /// such as domains or functions, do not generate any verify units. In these /// cases, `None` is returned. - pub fn from_source_unit(mut source_unit: SourceUnit, depgraph: &mut DepGraph) -> Option { - let deps = match &mut source_unit { - SourceUnit::Decl(decl) => depgraph.get_reachable([decl.name()]), - SourceUnit::Raw(block) => { - assert!(depgraph.current_deps.is_empty()); - depgraph.visit_block(block).unwrap(); - let current_deps = std::mem::take(&mut depgraph.current_deps); - depgraph.get_reachable(current_deps) - } - }; + pub fn from_proc_verify(mut proc_verify: SourceUnit, depgraph: &mut DepGraph) -> Option { + let deps = Self::compute_deps(&mut proc_verify, depgraph); - match source_unit { + match proc_verify { SourceUnit::Decl(decl) => { match decl { DeclKind::ProcDecl(proc_decl) => { let (direction, block) = encode_proc_verify(&proc_decl.borrow())?; - Some(CoreVerifyTask { + Some(CoreHeyVLTask { deps, direction, block, @@ -103,7 +95,7 @@ impl CoreVerifyTask { _ => unreachable!(), // axioms and variable declarations are not allowed on the top level } } - SourceUnit::Raw(block) => Some(CoreVerifyTask { + SourceUnit::Raw(block) => Some(CoreHeyVLTask { deps, direction: Direction::Down, block, @@ -111,6 +103,47 @@ impl CoreVerifyTask { } } + /// Same as [`from_proc_verify`] but translating from proc_pre_model. + /// For this the preexpectations need to be translated + pub fn from_proc_pre_model(mut proc_pre_model: SourceUnit, depgraph: &mut DepGraph) -> Option { + let deps = Self::compute_deps(&mut proc_pre_model, depgraph); + match proc_pre_model { + SourceUnit::Decl(decl) => { + match decl { + DeclKind::ProcDecl(proc_decl) => { + let (direction, block) = encode_preexpectation(&proc_decl.borrow())?; + Some(CoreHeyVLTask { + deps, + direction, + block, + }) + } + DeclKind::DomainDecl(_domain_decl) => None, // TODO: check that the axioms are not contradictions + DeclKind::FuncDecl(_func_decl) => None, + _ => unreachable!(), // axioms and variable declarations are not allowed on the top level + } + } + SourceUnit::Raw(block) => Some(CoreHeyVLTask { + deps, + direction: Direction::Down, + block, + }), + } + } + + /// Compute the dependency closure for a given source unit. + fn compute_deps(source_unit: &mut SourceUnit, depgraph: &mut DepGraph) -> Dependencies { + match source_unit { + SourceUnit::Decl(decl) => depgraph.get_reachable([decl.name()]), + SourceUnit::Raw(block) => { + assert!(depgraph.current_deps.is_empty()); + depgraph.visit_block(block).unwrap(); + let current_deps = std::mem::take(&mut depgraph.current_deps); + depgraph.get_reachable(current_deps) + } + } + } + /// Desugar assignments with procedure calls. #[instrument(skip_all)] pub fn desugar_spec_calls(&mut self, tcx: &mut TyCtx, name: String) -> Result<(), CaesarError> { @@ -196,7 +229,7 @@ fn top_lit_in_lattice(dir: Direction, ty: &TyKind) -> Expr { } } -impl SimplePretty for CoreVerifyTask { +impl SimplePretty for CoreHeyVLTask { fn pretty(&self) -> Doc { let lower_bounds = to_direction_lower_bounds(self.clone()); assert_eq!(lower_bounds.direction, Direction::Down); @@ -204,7 +237,7 @@ impl SimplePretty for CoreVerifyTask { } } -impl fmt::Display for CoreVerifyTask { +impl fmt::Display for CoreHeyVLTask { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { self.pretty().render_fmt(80, f) } diff --git a/src/driver/mod.rs b/src/driver/mod.rs index 10b862c3..43580107 100644 --- a/src/driver/mod.rs +++ b/src/driver/mod.rs @@ -1,7 +1,7 @@ //! This module glues all components of Caesar together. pub mod commands; -pub mod core_verify; +pub mod core_heyvl; pub mod error; pub mod front; pub mod item; diff --git a/src/driver/smt_proof.rs b/src/driver/smt_proof.rs index 098c5884..eb9de814 100644 --- a/src/driver/smt_proof.rs +++ b/src/driver/smt_proof.rs @@ -6,6 +6,7 @@ use std::io::Write; use ariadne::ReportKind; use itertools::Itertools; use tracing::info_span; +use z3::SatResult; use z3::{ ast::{Ast, Bool}, Context, Goal, @@ -48,7 +49,8 @@ use crate::{ }, smt::{ pretty_model::{ - pretty_model, pretty_slice, pretty_unaccessed, pretty_var_value, pretty_vc_value, + pretty_model, pretty_nontrivial_model, pretty_slice, pretty_unaccessed, + pretty_var_value, pretty_vc_value, }, translate_exprs::TranslateExprs, }, @@ -167,6 +169,86 @@ pub fn run_smt_prove_task( Ok(result.prove_result) } +/// Run the SMT satisfiability check: translate the verification condition to Z3, +/// add axioms and assumptions, check if its sat and find a model, +/// print the result and model and return the result. +pub fn run_smt_check_sat<'tcx>( + options: &VerifyCommand, + limits_ref: &LimitsRef, + tcx: &'tcx TyCtx, + depgraph: &DepGraph, + name: &SourceUnitName, + bool_task: BoolVcProveTask, + server: &mut dyn Server, +) -> Result { + let ctx = Context::new(&z3::Config::default()); + let function_encoder = mk_function_encoder(tcx, depgraph, options)?; + let dep_config = DepConfig::Set(bool_task.get_dependencies()); + let smt_ctx = SmtCtx::new(&ctx, tcx, function_encoder, dep_config); + let mut translate = TranslateExprs::new(&smt_ctx); + let mut vc_is_valid = SmtVcProveTask::translate(bool_task, &mut translate); + + if !options.opt_options.no_simplify { + vc_is_valid.simplify(); + } + + if options.debug_options.z3_trace { + tracing::info!("Z3 tracing output will be written to `z3.log`."); + } + + let mut prover = Prover::new(&ctx, IncrementalMode::Native); + + if let Some(remaining) = limits_ref.time_left() { + prover.set_timeout(remaining); + } + + // Add axioms and assumptions + translate.ctx.add_lit_axioms_to_prover(&mut prover); + translate + .ctx + .uninterpreteds() + .add_axioms_to_prover(&mut prover); + translate + .local_scope() + .add_assumptions_to_prover(&mut prover); + + // Add the verification condition. This should be checked for satisfiability. + // Therefore, add_assumption is used (which just adds it as an smtlib assert) + // vs. add_provable, which would negate it first. + prover.add_assumption(&vc_is_valid.vc); + + // Optionally dump SMT-LIB representation + if let Some(smtlib) = get_smtlib(options, &prover) { + write_smtlib(&options.debug_options, name, &smtlib, None)?; + } + + // Run solver & retrieve model if available + let sat_result = prover.check_sat(); + let model = prover.get_model(); + + let files = server.get_files_internal().lock().unwrap(); + match &sat_result { + SatResult::Sat => { + println!("{name}: A non-trivial bound is given for example by the following model:"); + let model = model.as_ref().unwrap(); + let mut w = Vec::new(); + let doc = pretty_nontrivial_model(&files, &vc_is_valid.quant_vc, &mut translate, model); + doc.nest(4).render(120, &mut w).unwrap(); + println!(" {}", String::from_utf8(w).unwrap()); + } + SatResult::Unsat => { + println!( + "{name}: The bound introduced by the preexpectations is always trivial (bottom for proc/top for coproc)" + ); + } + SatResult::Unknown => { + println!("{name}: Unknown result!"); + } + } + + Ok(sat_result) +} + /// Create the function encoder based on the given command's options. pub fn mk_function_encoder<'ctx>( tcx: &TyCtx, diff --git a/src/procs/proc_verify.rs b/src/procs/proc_verify.rs index 5e8bad7d..adcc9a27 100644 --- a/src/procs/proc_verify.rs +++ b/src/procs/proc_verify.rs @@ -1,9 +1,59 @@ use crate::{ - ast::{Block, Direction, ProcDecl, SpanVariant, Spanned, StmtKind}, - driver::core_verify::CoreVerifyTask, + ast::{ + BinOpKind, Block, Direction, ExprData, ExprKind, ProcDecl, Shared, Span, SpanVariant, + Spanned, StmtKind, TyKind, + }, + driver::core_heyvl::CoreHeyVLTask, slicing::{wrap_with_error_message, wrap_with_success_message}, }; +/// Encode the preexpectations as a formula for which a model is a nontrivial bound. +/// +/// For proc: +/// goal: Find a model such that (pre1 ⊓ pre2 ⊓...) > 0 +/// For coproc: +/// goal: Find a model such that (pre1 ⊔ pre2 ⊔...) < top +pub fn encode_preexpectation(proc: &ProcDecl) -> Option<(Direction, Block)> { + let direction = proc.direction; + + let body_ref = proc.body.borrow(); + let body = match &*body_ref { + Some(body) => body, + None => return None, + }; + let mut block = Spanned::new(body.span, vec![]); + + fn get_combination(direction: Direction) -> BinOpKind { + let combination = match direction { + Direction::Down => BinOpKind::Inf, + Direction::Up => BinOpKind::Sup, + }; + combination + } + + // Combine the preexpectations using the correct operator + let build_expr = proc + .requires() + .cloned() + .reduce(|lhs, rhs| { + Shared::new(ExprData { + kind: ExprKind::Binary( + Spanned::with_dummy_span(get_combination(direction)).clone(), + lhs, + rhs, + ), + ty: Some(TyKind::EUReal), + span: Span::dummy_span(), + }) + }) + .expect("No preconditions to check"); + + block.node.push(Spanned::new( + Span::dummy_span(), + StmtKind::Assert(direction, build_expr), + )); + Some((direction, block)) +} /// Generates the HeyVL code to verify a procedure implementation. Returns /// `None` if the proc has no body does not need verification. /// @@ -71,7 +121,7 @@ pub fn encode_proc_verify(proc: &ProcDecl) -> Option<(Direction, Block)> { /// This is currently not used in the code anymore as we want to track the /// direction explicitly to have better error messages, but exists for the sake /// of completeness. -pub fn to_direction_lower_bounds(mut verify_unit: CoreVerifyTask) -> CoreVerifyTask { +pub fn to_direction_lower_bounds(mut verify_unit: CoreHeyVLTask) -> CoreHeyVLTask { if verify_unit.direction == Direction::Up { verify_unit.direction = Direction::Down; verify_unit.block.node.insert( diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs index 00c2f72f..e8fd9a4a 100644 --- a/src/smt/pretty_model.rs +++ b/src/smt/pretty_model.rs @@ -47,6 +47,46 @@ pub fn pretty_model<'smt, 'ctx>( Doc::intersperse(res, Doc::line_().append(Doc::line_())).append(Doc::line_()) } +/// Pretty-print a model for get models. +pub fn pretty_nontrivial_model<'smt, 'ctx>( + files: &Files, + vc_expr: &QuantVcProveTask, + translate: &mut TranslateExprs<'smt, 'ctx>, + model: &InstrumentedModel<'ctx>, +) -> Doc { + let mut res: Vec = vec![]; + + // Print the values of the global variables in the model. + pretty_globals(translate, model, files, &mut res); + + // Print the unaccessed definitions. + if let Some(unaccessed) = pretty_unaccessed(model) { + res.push(unaccessed); + } + + res.push(pretty_get_models_value(vc_expr, translate, model)); + + Doc::intersperse(res, Doc::line_().append(Doc::line_())).append(Doc::line_()) +} + +pub fn pretty_get_models_value<'smt, 'ctx>( + vc_expr: &QuantVcProveTask, + translate: &mut TranslateExprs<'smt, 'ctx>, + model: &InstrumentedModel<'ctx>, +) -> Doc { + let original_program_vc = vc_expr.expr.clone(); + let mut lines = vec![]; + + let ast = translate.t_symbolic(&original_program_vc); + let value = ast.eval(model); + let res = pretty_eval_result(value); + lines.push( + Doc::text("the pre-quantity evaluated to:").append(Doc::hardline().append(res).nest(4)), + ); + + Doc::intersperse(lines, Doc::line()) +} + pub fn pretty_vc_value<'smt, 'ctx>( vc_expr: &QuantVcProveTask, translate: &mut TranslateExprs<'smt, 'ctx>,