From bb3fe37d169f40bb2bd940969328c181279df5c0 Mon Sep 17 00:00:00 2001 From: ole-thoeb <43213977+ole-thoeb@users.noreply.github.com> Date: Mon, 4 Nov 2024 18:27:51 +0100 Subject: [PATCH] Address most of the PR feedback --- src/main.rs | 1 + src/smt/limited.rs | 90 ++++++++++++++++++++++++++++++++++++++ src/smt/mod.rs | 51 +++++---------------- src/smt/translate_exprs.rs | 5 +++ z3rro/src/lit.rs | 10 +++-- 5 files changed, 115 insertions(+), 42 deletions(-) create mode 100644 src/smt/limited.rs diff --git a/src/main.rs b/src/main.rs index 06207b2a..38592fee 100644 --- a/src/main.rs +++ b/src/main.rs @@ -184,6 +184,7 @@ pub struct Options { pub jani_skip_quant_pre: bool, /// Limit the number of times a function declaration can be recursively instantiated. + /// Requires that MBQI is disabled with `force-ematching`. #[structopt(long)] pub limited_functions: bool, diff --git a/src/smt/limited.rs b/src/smt/limited.rs new file mode 100644 index 00000000..acca70e9 --- /dev/null +++ b/src/smt/limited.rs @@ -0,0 +1,90 @@ +//! This module contains all functions related to fuel encoding from the paper +//! "Computing with an SMT Solver". The goal is to limit the number of quantifier instantiation +//! of a functions defining axiom. This is done by including an extra [z3rro::Fuel] parameter and +//! only providing axioms for non-zero fuel parameters. The fuel parameter is decremented in every +//! instantiation. +//! +//! # Note +//! For this to work the SMT solver is not allowed to synthesis fuel values itself. +//! Therefore, MBQI must be disabled. + +use crate::ast::{Expr, FuncDecl}; +use crate::smt::translate_exprs::{FuelContext, TranslateExprs}; +use crate::smt::{ty_to_sort, SmtCtx}; +use z3::ast::{Ast, Bool}; +use z3::{Pattern, Sort}; +use z3rro::SmtEq; + +/// Builds the domain (parameter list) for `func`. If the limited function transformation is +/// applicable a fuel parameter is implicitly added as the first parameter. +pub fn build_func_domain<'a>(ctx: &SmtCtx<'a>, func: &FuncDecl) -> Vec> { + let mut domain = if ctx.is_limited_function_decl(func) { + vec![ctx.fuel_factory().sort().clone()] + } else { + vec![] + }; + domain.extend( + func.inputs + .node + .iter() + .map(|param| ty_to_sort(ctx, ¶m.ty)), + ); + domain +} + +/// Creates an axiom that can only be instantiated with a non-zero fuel parameter and decrements +/// the available fuel in the body. +/// It has the form: +/// ```txt +/// forall fuel: Fuel, . func_name(Succ(fuel), ) = func_name(fuel, ) +/// ``` +fn translate_defining_axiom<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + lhs: &Expr, + rhs: &Expr, +) -> Bool<'ctx> { + translate.push(); + translate.set_fuel_context(FuelContext::Head); + + let symbolic_lhs = translate.t_symbolic(lhs).into_dynamic(translate.ctx); + translate.set_fuel_context(FuelContext::Body); + let symbolic_rhs = translate.t_symbolic(rhs).into_dynamic(translate.ctx); + + let axiom = translate.local_scope().forall( + &[&Pattern::new( + translate.ctx.ctx, + &[&symbolic_lhs as &dyn Ast<'ctx>], + )], + &symbolic_lhs.smt_eq(&symbolic_rhs), + ); + + translate.set_fuel_context(FuelContext::Call); // reset to default + translate.pop(); + + axiom +} + +/// Creates the fuel synonym axiom that states that the result of the function is independent +/// of the fuel parameter. It has the form: +/// ```txt +/// forall fuel: Fuel, . func_name(Succ(fuel), ) = func_name(fuel, ) +/// ``` +pub fn fuel_synonym_axiom<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + app: &Expr, +) -> Bool<'ctx> { + translate_defining_axiom(translate, app, app) +} + +/// Creates the default defining axiom for a function. It has the form: +/// ```txt +/// forall fuel: Fuel, . func_name(Succ(fuel), ) = +/// ``` +/// where only `fuel` is used as the fuel parameter in ``. +pub fn defining_axiom<'smt, 'ctx>( + translate: &mut TranslateExprs<'smt, 'ctx>, + app: &Expr, + body: &Expr, +) -> Bool<'ctx> { + translate_defining_axiom(translate, app, body) +} diff --git a/src/smt/mod.rs b/src/smt/mod.rs index e862a895..8c014e4b 100644 --- a/src/smt/mod.rs +++ b/src/smt/mod.rs @@ -11,7 +11,8 @@ use z3rro::{ }; use self::{translate_exprs::TranslateExprs, uninterpreted::Uninterpreteds}; -use crate::ast::{DeclKind, Expr, FuncDecl}; +use crate::ast::{DeclKind, FuncDecl}; +use crate::smt::limited::{build_func_domain, defining_axiom, fuel_synonym_axiom}; use crate::smt::symbolic::Symbolic; use crate::smt::translate_exprs::FuelContext; use crate::{ @@ -19,6 +20,7 @@ use crate::{ tyctx::TyCtx, }; +mod limited; pub mod pretty_model; pub mod symbolic; mod symbols; @@ -74,20 +76,7 @@ impl<'ctx> SmtCtx<'ctx> { if let DomainSpec::Function(func_ref) = &spec { let func = func_ref.borrow(); - let mut domain = if self.is_limited_function_decl(&func) { - // For function definitions we constrain the number - // of quantifier installations through a fuel parameter. - // The fuel parameter is automatically added as the first parameter. - vec![self.fuel_factory().sort().clone()] - } else { - vec![] - }; - domain.extend( - func.inputs - .node - .iter() - .map(|param| ty_to_sort(self, ¶m.ty)), - ); + let domain = build_func_domain(self, &func); let domain: Vec<&Sort<'_>> = domain.iter().collect(); let range = ty_to_sort(self, &func.output); self.uninterpreteds.add_function(func.name, &domain, &range); @@ -139,34 +128,15 @@ impl<'ctx> SmtCtx<'ctx> { translate.pop(); } - let mut add_defining_axiom = |name: Ident, lhs: &Expr, rhs: &Expr| { - translate.push(); - translate.set_fuel_context(FuelContext::Head); - let symbolic_lhs = translate.t_symbolic(lhs).into_dynamic(self); - - translate.set_fuel_context(FuelContext::Body); - let symbolic_rhs = translate.t_symbolic(rhs).into_dynamic(self); - - axioms.push(( - name, - translate.local_scope().forall( - &[&Pattern::new(self.ctx, &[&symbolic_lhs as &dyn Ast<'ctx>])], - &symbolic_lhs.smt_eq(&symbolic_rhs), - ), - )); - translate.set_fuel_context(FuelContext::Call); - translate.pop(); - }; - if self.is_limited_function_decl(&func) { - // fuel synonym axiom - add_defining_axiom(func.name, &app, &app); // TODO: create a new name for the axiom + // TODO: create a new name for the axiom + axioms.push((func.name, fuel_synonym_axiom(&mut translate, &app))); } // create the axiom for the definition if there is a body if let Some(body) = &*body { - // Defining axiom - add_defining_axiom(func.name, &app, body); // TODO: create a new name for the axiom + // TODO: create a new name for the axiom + axioms.push((func.name, defining_axiom(&mut translate, &app, body))); // Computing axiom if self.lit_wrap { @@ -281,7 +251,7 @@ impl<'ctx> SmtCtx<'ctx> { } } -fn ty_to_sort<'ctx>(ctx: &SmtCtx<'ctx>, ty: &TyKind) -> Sort<'ctx> { +pub fn ty_to_sort<'ctx>(ctx: &SmtCtx<'ctx>, ty: &TyKind) -> Sort<'ctx> { match ty { TyKind::Bool => Sort::bool(ctx.ctx()), TyKind::Int | TyKind::UInt => Sort::int(ctx.ctx()), @@ -301,6 +271,7 @@ fn ty_to_sort<'ctx>(ctx: &SmtCtx<'ctx>, ty: &TyKind) -> Sort<'ctx> { } } +/// A [LitDecl] wrapper providing a simpler and better typed interface. pub enum Lit<'ctx> { Disabled, Enabled { decl: LitDecl<'ctx>, ty: TyKind }, @@ -318,6 +289,8 @@ impl<'ctx> Lit<'ctx> { Self::Disabled } + /// Wrap a value in a `Lit` marker if the functionality is enabled. Otherwise, return the + /// argument directly. pub fn wrap(&self, ctx: &SmtCtx<'ctx>, arg: A) -> A where A: Into> + TryFrom>, diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs index 91735ca3..9892b4c9 100644 --- a/src/smt/translate_exprs.rs +++ b/src/smt/translate_exprs.rs @@ -775,6 +775,11 @@ impl<'ctx> FuelContextInternal<'ctx> { } } +/// Lazily initialised [ScopeSymbolic] of type [Fuel]. It is initialised when a limited function is +/// encountered in context that requires a fresh quantified fuel variable ([FuelContext::Head], +/// [FuelContext::Body]). It is discarded when the context changes back to [FuelContext::Call] +/// (see [TranslateExprs::set_fuel_context]). The lazy initialisation ensures that the fuel variable +/// is only added to the quantifier if it is actually used. #[derive(Default)] struct QuantifiedFuel<'ctx>(OnceCell>); diff --git a/z3rro/src/lit.rs b/z3rro/src/lit.rs index 176f6cd6..769d1c23 100644 --- a/z3rro/src/lit.rs +++ b/z3rro/src/lit.rs @@ -3,6 +3,13 @@ use std::fmt::Debug; use z3::ast::{Ast, Dynamic}; use z3::{Context, Sort}; +/// Identity function that is used to mark constants values. They allow for axioms instantiation +/// without consuming fuel. This allows the SMT to still compute the result of functions where the +/// arguments are known, while limiting instantiation in other cases. +/// +/// Conceptually the `Lit` function is generic over its argument. For encoding into SMT it must be +/// monomorphized. A [LitDecl] instance represents a concrete monomorphization and is parameterised +/// by the z3 sort of the argument/ return value. #[derive(Debug)] pub struct LitDecl<'ctx> { _ctx: &'ctx Context, @@ -10,9 +17,6 @@ pub struct LitDecl<'ctx> { func: FuncDef<'ctx>, } -/// Identity function that is used to mark constants values. They allow for axioms instantiation -/// without consuming fuel. This allows the SMT to still compute the result of functions where the -/// arguments are known, while limiting instantiation in other cases. impl<'ctx> LitDecl<'ctx> { pub fn new(ctx: &'ctx Context, arg_sort: Sort<'ctx>) -> Self { // TODO: How do we avoid clashes with user defined code?