From f944bea53990e258c5337b0e7edc6897d89bb265 Mon Sep 17 00:00:00 2001
From: Emil <eloemil@yahoo.de>
Date: Fri, 3 Jan 2025 19:15:36 +0100
Subject: [PATCH] Do not lit-wrap if we can not profit from it

---
 src/ast/decl.rs    |  9 +++++++++
 src/smt/limited.rs |  6 ++++++
 src/smt/mod.rs     | 16 ++++++++++++----
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/src/ast/decl.rs b/src/ast/decl.rs
index a85826f8..52749ded 100644
--- a/src/ast/decl.rs
+++ b/src/ast/decl.rs
@@ -444,6 +444,15 @@ pub struct DomainDecl {
     pub span: Span,
 }
 
+impl DomainDecl {
+    pub fn function_decls(&self) -> impl Iterator<Item = &DeclRef<FuncDecl>> {
+        self.body.iter().filter_map(|spec| match spec {
+            DomainSpec::Function(func_ref) => Some(func_ref),
+            _ => None,
+        })
+    }
+}
+
 impl SimplePretty for DomainDecl {
     fn pretty(&self) -> Doc {
         Doc::text("domain")
diff --git a/src/smt/limited.rs b/src/smt/limited.rs
index dee2c779..71d400e5 100644
--- a/src/smt/limited.rs
+++ b/src/smt/limited.rs
@@ -260,6 +260,12 @@ pub fn return_value_invariant<'smt, 'ctx>(
     axiom
 }
 
+/// Returns true if the [FuncDecl] can be transformed into a limited function.
+/// Use [SmtCtx::is_limited_function_decl] to check if the transformation should actually be applied.
+pub fn is_eligible_for_limited_function(func: &FuncDecl) -> bool {
+    func.body.borrow().is_some()
+}
+
 type HashExpr = PointerHashShared<ExprData>;
 
 #[derive(Default, Clone)]
diff --git a/src/smt/mod.rs b/src/smt/mod.rs
index 6e0659b8..c09e9356 100644
--- a/src/smt/mod.rs
+++ b/src/smt/mod.rs
@@ -4,7 +4,7 @@ use self::{translate_exprs::TranslateExprs, uninterpreted::Uninterpreteds};
 use crate::ast::{DeclKind, FuncDecl};
 use crate::smt::limited::{
     build_func_domain, computation_axiom, defining_axiom, fuel_synonym_axiom,
-    return_value_invariant,
+    is_eligible_for_limited_function, return_value_invariant,
 };
 use crate::{
     ast::{DeclRef, DomainDecl, DomainSpec, Ident, TyKind},
@@ -48,6 +48,15 @@ pub struct SmtCtx<'ctx> {
 
 impl<'ctx> SmtCtx<'ctx> {
     pub fn new(ctx: &'ctx Context, tcx: &'ctx TyCtx, options: SmtCtxOptions) -> Self {
+        let domains: Vec<_> = tcx.domains_owned();
+        // disable lit-wrapping if there are no limited functions that can profit from it
+        let lit_wrap = options.lit_wrap
+            && options.use_limited_functions
+            && domains.iter().any(|d| {
+                d.borrow()
+                    .function_decls()
+                    .any(|func| is_eligible_for_limited_function(&func.borrow()))
+            });
         let mut res = SmtCtx {
             ctx,
             tcx,
@@ -57,9 +66,8 @@ impl<'ctx> SmtCtx<'ctx> {
             lits: RefCell::new(Vec::new()),
             uninterpreteds: Uninterpreteds::new(ctx),
             use_limited_functions: options.use_limited_functions,
-            lit_wrap: options.lit_wrap,
+            lit_wrap,
         };
-        let domains: Vec<_> = tcx.domains_owned();
         res.declare_domains(domains.as_slice());
         res
     }
@@ -204,7 +212,7 @@ impl<'ctx> SmtCtx<'ctx> {
     }
 
     pub fn is_limited_function_decl(&self, func: &FuncDecl) -> bool {
-        self.use_limited_functions && func.body.borrow().is_some()
+        self.use_limited_functions && is_eligible_for_limited_function(func)
     }
 
     pub fn functions_with_def(&self) -> Vec<Ident> {