Limited functions

.gitignore

@@ -1,4 +1,5 @@
 target
+.idea
 .DS_Store
 benchmark-results.csv
 vscode-ext/node_modules/

Cargo.toml

@@ -13,9 +13,10 @@ edition = "2021"
 build = "build.rs" # LALRPOP preprocessing
 
 [features]
-default = ["static-link-z3"]
+default = ["static-link-z3", "datatype-fuel"]
 datatype-eureal = ["z3rro/datatype-eureal"]
 datatype-eureal-funcs = ["z3rro/datatype-eureal-funcs"]
+datatype-fuel=["z3rro/datatype-fuel"]
 static-link-z3 = ["z3/static-link-z3"]
 # Emit log messages to stderr without timing information. This is useful to diff logs.
 log-print-timeless = []
@@ -80,8 +81,8 @@ harness = false
 opt-level = 3
 
 [patch.crates-io]
-z3 = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
-z3-sys = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
+z3 = { git = 'https://github.com/prove-rs/z3.rs.git', rev = '60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf' }
+z3-sys = { git = 'https://github.com/prove-rs/z3.rs.git', rev = '60001b36fc8a7ab1d4f22595e80a3b6f7adc1bcf' }
 # to work on z3.rs locally, clone it into the main directory and use the following directive instead:
 # z3 = { path = 'z3.rs/z3' }
 

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")

src/ast/expr.rs

@@ -66,6 +66,21 @@ pub enum ExprKind {
     Lit(Lit),
 }
 
+impl Expr {
+    pub fn children_mut(&mut self) -> Vec<&mut Expr> {
+        match &mut self.kind {
+            ExprKind::Var(_) | ExprKind::Lit(_) => vec![],
+            ExprKind::Call(_, args) => args.iter_mut().collect(),
+            ExprKind::Ite(cond, branch1, branch2) => vec![cond, branch1, branch2],
+            ExprKind::Binary(_, lhs, rhs) => vec![lhs, rhs],
+            ExprKind::Unary(_, operand) => vec![operand],
+            ExprKind::Cast(operand) => vec![operand],
+            ExprKind::Quant(_, _, _, expr) => vec![expr],
+            ExprKind::Subst(_, subst, expr) => vec![subst, expr],
+        }
+    }
+}
+
 impl SimplePretty for Expr {
     fn pretty(&self) -> Doc {
         let res = match &self.kind {

src/ast/shared.rs

@@ -1,3 +1,6 @@
+use ref_cast::RefCast;
+use std::cmp::Ordering;
+use std::hash::{Hash, Hasher};
 use std::{
     fmt,
     ops::{Deref, DerefMut},
@@ -72,3 +75,48 @@ impl<T: ?Sized + fmt::Debug> fmt::Debug for Shared<T> {
         fmt::Debug::fmt(&**self, f)
     }
 }
+
+/// [Shared] wrapper that provides pointer based [Eq] and [Hash] implementations.
+#[repr(transparent)]
+#[derive(RefCast, Clone)]
+pub struct PointerHashShared<T>(Shared<T>);
+
+impl<T> PointerHashShared<T> {
+    pub fn new(shared: Shared<T>) -> Self {
+        Self(shared)
+    }
+
+    pub fn into_shared(self) -> Shared<T> {
+        self.0
+    }
+
+    pub fn as_shared(&self) -> &Shared<T> {
+        &self.0
+    }
+}
+
+impl<T> PartialEq for PointerHashShared<T> {
+    fn eq(&self, other: &Self) -> bool {
+        Shared::as_ptr(&self.0) == Shared::as_ptr(&other.0)
+    }
+}
+
+impl<T> Eq for PointerHashShared<T> {}
+
+impl<T> Ord for PointerHashShared<T> {
+    fn cmp(&self, other: &Self) -> Ordering {
+        Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0))
+    }
+}
+
+impl<T> PartialOrd for PointerHashShared<T> {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(Shared::as_ptr(&self.0).cmp(&Shared::as_ptr(&other.0)))
+    }
+}
+
+impl<T> Hash for PointerHashShared<T> {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        Shared::as_ptr(&self.0).hash(state)
+    }
+}

src/driver.rs

@@ -68,6 +68,7 @@ use z3rro::{
     util::{PrefixWriter, ReasonUnknown},
 };
 
+use crate::smt::{LiteralExprCollector, SmtCtxOptions};
 use tracing::{info_span, instrument, trace};
 
 /// Human-readable name for a source unit. Used for debugging and error messages.
@@ -535,7 +536,7 @@ impl QuantVcUnit {
         let _entered = span.enter();
         if !options.opt_options.strict {
             let ctx = Context::new(&Config::default());
-            let smt_ctx = SmtCtx::new(&ctx, tcx);
+            let smt_ctx = SmtCtx::new(&ctx, tcx, SmtCtxOptions::default());
             let mut unfolder = Unfolder::new(limits_ref.clone(), &smt_ctx);
             unfolder.visit_expr(&mut self.expr)
         } else {
@@ -633,14 +634,23 @@ impl BoolVcUnit {
 
     /// Translate to SMT.
     pub fn into_smt_vc<'smt, 'ctx>(
-        self,
+        mut self,
         translate: &mut TranslateExprs<'smt, 'ctx>,
     ) -> SmtVcUnit<'ctx> {
         let span = info_span!("translation to Z3");
         let _entered = span.enter();
+
+        translate.set_literal_exprs(
+            LiteralExprCollector::new()
+                .with_functions_with_def(translate.ctx.functions_with_def().as_slice())
+                .collect(&mut self.vc),
+        );
+        let bool_vc = translate.t_bool(&self.vc);
+        translate.clear_literal_exprs();
+
         SmtVcUnit {
             quant_vc: self.quant_vc,
-            vc: translate.t_bool(&self.vc),
+            vc: bool_vc,
         }
     }
 }
@@ -689,7 +699,7 @@ impl<'ctx> SmtVcUnit<'ctx> {
             });
         }
 
-        let mut slice_solver = SliceSolver::new(slice_vars.clone(), translate, prover);
+        let slice_solver = SliceSolver::new(slice_vars.clone(), translate, prover);
         let failing_slice_options = SliceSolveOptions {
             globally_optimal: !options.slice_options.slice_error_first,
             continue_on_unknown: false,
@@ -769,6 +779,8 @@ fn mk_valid_query_prover<'smt, 'ctx>(
         prover.set_timeout(remaining);
     }
 
+    // add the definition of all used Lit marker functions
+    smt_translate.ctx.add_lit_axioms_to_prover(&mut prover);
     // add assumptions (from axioms and locals) to the prover
     smt_translate
         .ctx

src/main.rs

@@ -14,6 +14,7 @@ use std::{
     time::{Duration, Instant},
 };
 
+use crate::smt::SmtCtxOptions;
 use crate::{
     ast::TyKind,
     driver::mk_z3_ctx,
@@ -35,7 +36,6 @@ use thiserror::Error;
 use timing::DispatchBuilder;
 use tokio::task::JoinError;
 use tracing::{error, info, warn};
-
 use vc::explain::VcExplanation;
 use z3rro::{prover::ProveResult, util::ReasonUnknown};
 
@@ -158,6 +158,25 @@ pub struct OptimizationOptions {
     /// the current solver state.
     #[arg(long)]
     pub no_simplify: bool,
+
+    /// Limit the number of times a function declaration can be recursively instantiated.
+    /// Requires that MBQI is disabled with `force-ematching`.
+    #[arg(long)]
+    pub limited_functions: bool,
+
+    /// Force the SMT solver to only use emaching for quantifier instantiation, disabling mbqi.
+    #[arg(long)]
+    pub force_ematching: bool,
+
+    /// Do not count applications to constant values towards the instantiation count
+    /// when using `limited-functions`.
+    #[arg(long)]
+    pub lit_wrap: bool,
+
+    /// For each function f Generate multiple function f_n (f_2, f_1, f_0) that each respectively
+    /// can only be instantiated n times. Requires `limited-functions`
+    #[arg(long)]
+    pub static_fuel: bool,
 }
 
 #[derive(Debug, Default, Args)]
@@ -232,6 +251,10 @@ pub struct DebugOptions {
     /// Enable Z3 tracing for the final SAT check.
     #[arg(long)]
     pub z3_trace: bool,
+
+    /// An explicit seed used by Z3 for the final SAT check.
+    #[arg(long)]
+    pub z3_seed: Option<u32>,
 }
 
 #[derive(Debug, Default, Args)]
@@ -634,6 +657,9 @@ fn verify_files_main(
         warn!("Z3 tracing is enabled with multiple verification units. Intermediate tracing results will be overwritten.");
     }
 
+    // set requested global z3 options
+    set_global_z3_options(options, &limits_ref);
+
     let mut num_proven: usize = 0;
     let mut num_failures: usize = 0;
 
@@ -698,7 +724,15 @@ fn verify_files_main(
 
         // 11. Translate to Z3
         let ctx = mk_z3_ctx(options);
-        let smt_ctx = SmtCtx::new(&ctx, &tcx);
+        let smt_ctx = SmtCtx::new(
+            &ctx,
+            &tcx,
+            SmtCtxOptions {
+                use_limited_functions: options.opt_options.limited_functions,
+                lit_wrap: options.opt_options.lit_wrap,
+                static_fuel: options.opt_options.static_fuel,
+            },
+        );
         let mut translate = TranslateExprs::new(&smt_ctx);
         let mut vc_is_valid = vc_is_valid.into_smt_vc(&mut translate);
 
@@ -773,3 +807,22 @@ fn print_timings() {
         .collect();
     eprintln!("Timings: {:?}", timings);
 }
+
+fn set_global_z3_options(options: &Options, limits_ref: &LimitsRef) {
+    // the parameters are set as globals since params set via (Solver::set_params) sometimes get ignored.
+
+    // default
+    z3::set_global_param("smt.qi.eager_threshold", "100");
+    z3::set_global_param("smt.qi.lazy_threshold", "1000");
+    if options.opt_options.force_ematching {
+        // z3::set_global_param("auto-config", "false");
+        // z3::set_global_param("smt.mbqi", "false");
+        z3::set_global_param("smt.mbqi.id", "mbqi");
+    }
+    if let Some(seed) = options.debug_options.z3_seed {
+        z3::set_global_param("smt.random_seed", &seed.to_string());
+    }
+    if let Some(timeout) = limits_ref.time_left() {
+        z3::set_global_param("timeout", &timeout.as_millis().to_string())
+    }
+}

src/opt/fuzz_test.rs

@@ -4,6 +4,7 @@ use proptest::{
 };
 use z3rro::prover::{ProveResult, Prover};
 
+use crate::smt::SmtCtxOptions;
 use crate::{
     ast::{
         BinOpKind, DeclKind, DeclRef, Expr, ExprBuilder, ExprData, ExprKind, Ident, LitKind,
@@ -198,7 +199,7 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult {
         optimized.clone(),
     );
     let ctx = z3::Context::new(&z3::Config::new());
-    let smt_ctx = SmtCtx::new(&ctx, tcx);
+    let smt_ctx = SmtCtx::new(&ctx, tcx, SmtCtxOptions::default());
     let mut translate = TranslateExprs::new(&smt_ctx);
     let eq_expr_z3 = translate.t_bool(&eq_expr);
     let mut prover = Prover::new(&ctx);

src/opt/unfolder.rs

@@ -275,6 +275,7 @@ fn negate_expr(expr: Expr) -> Expr {
 #[cfg(test)]
 mod test {
     use super::Unfolder;
+    use crate::smt::SmtCtxOptions;
     use crate::{
         ast::visit::VisitorMut, fuzz_expr_opt_test, opt::fuzz_test, resource_limits::LimitsRef,
         smt::SmtCtx,
@@ -285,7 +286,7 @@ mod test {
         fuzz_expr_opt_test!(|mut expr| {
             let tcx = fuzz_test::mk_tcx();
             let z3_ctx = z3::Context::new(&z3::Config::default());
-            let smt_ctx = SmtCtx::new(&z3_ctx, &tcx);
+            let smt_ctx = SmtCtx::new(&z3_ctx, &tcx, SmtCtxOptions::default());
             let limits_ref = LimitsRef::new(None);
             let mut unfolder = Unfolder::new(limits_ref, &smt_ctx);
             unfolder.visit_expr(&mut expr).unwrap();