Skip to content

Commit

Permalink
Add --static-fuel flag
Browse files Browse the repository at this point in the history
In the process the fuel encoding code was
completely restructured
  • Loading branch information
ole-thoeb committed Feb 10, 2025
1 parent 68c1680 commit a85d589
Show file tree
Hide file tree
Showing 8 changed files with 722 additions and 359 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ edition = "2021"
build = "build.rs" # LALRPOP preprocessing

[features]
default = ["static-link-z3", "datatype-fuel"]
default = ["datatype-fuel"]
datatype-eureal = ["z3rro/datatype-eureal"]
datatype-eureal-funcs = ["z3rro/datatype-eureal-funcs"]
datatype-fuel=["z3rro/datatype-fuel"]
Expand Down
6 changes: 6 additions & 0 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,11 @@ pub struct OptimizationOptions {
/// 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)]
Expand Down Expand Up @@ -725,6 +730,7 @@ fn verify_files_main(
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);
Expand Down
Loading

0 comments on commit a85d589

Please sign in to comment.