Address most of the PR feedback

moves-rwth · Nov 5, 2024 · bb3fe37 · bb3fe37
1 parent 72a65bb
commit bb3fe37
Show file tree

Hide file tree

Showing 5 changed files with 115 additions and 42 deletions.
diff --git 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
@@ -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<Sort<'a>> {
+    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, &param.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, <args...> . func_name(Succ(fuel), <args...>) = <body...> func_name(fuel, <args...>) <body...>
+/// ```
+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, <args...> . func_name(Succ(fuel), <args...>) = func_name(fuel, <args...>)
+/// ```
+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, <args...> . func_name(Succ(fuel), <args...>) = <body>
+/// ```
+/// where only `fuel` is used as the fuel parameter in `<body>`.
+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
@@ -11,14 +11,16 @@ 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::{
     ast::{DeclRef, DomainDecl, DomainSpec, ExprBuilder, Ident, SpanVariant, TyKind},
     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, &param.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<A>(&self, ctx: &SmtCtx<'ctx>, arg: A) -> A
     where
         A: Into<Symbolic<'ctx>> + TryFrom<Symbolic<'ctx>>,

diff --git 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<ScopeSymbolic<'ctx>>);
 

diff --git a/z3rro/src/lit.rs b/z3rro/src/lit.rs
@@ -3,16 +3,20 @@ 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,
     arg_sort: Sort<'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?