feat(symbolic): Seq, powerset, choose, keys/values, strings, compound dicts

specl/crates/specl-cli/src/main.rs

@@ -176,6 +176,10 @@ enum Commands {
         #[arg(long)]
         smart: bool,
 
+        /// Maximum sequence length for symbolic Seq[T] variables (default: 5)
+        #[arg(long, default_value = "5")]
+        seq_bound: usize,
+
         /// Show verbose output
         #[arg(short, long)]
         verbose: bool,
@@ -279,10 +283,20 @@ fn main() {
             k_induction,
             ic3,
             smart,
+            seq_bound,
             verbose,
         } => {
             if symbolic || inductive || k_induction.is_some() || ic3 || smart {
-                cmd_check_symbolic(&file, &constant, depth, inductive, k_induction, ic3, smart)
+                cmd_check_symbolic(
+                    &file,
+                    &constant,
+                    depth,
+                    inductive,
+                    k_induction,
+                    ic3,
+                    smart,
+                    seq_bound,
+                )
             } else {
                 cmd_check(
                     &file,
@@ -505,6 +519,7 @@ fn cmd_check_symbolic(
     k_induction: Option<usize>,
     ic3: bool,
     smart: bool,
+    seq_bound: usize,
 ) -> CliResult<()> {
     let filename = file.display().to_string();
     let source = Arc::new(fs::read_to_string(file).map_err(|e| CliError::IoError {
@@ -539,6 +554,7 @@ fn cmd_check_symbolic(
             SymbolicMode::Bmc
         },
         depth,
+        seq_bound,
     };
 
     let mode_str = if smart {

specl/crates/specl-symbolic/src/bmc.rs

@@ -15,10 +15,11 @@ pub fn check_bmc(
     spec: &CompiledSpec,
     consts: &[Value],
     max_depth: usize,
+    seq_bound: usize,
 ) -> SymbolicResult<SymbolicOutcome> {
     info!(depth = max_depth, "starting symbolic BMC");
 
-    let layout = VarLayout::from_spec(spec, consts)?;
+    let layout = VarLayout::from_spec(spec, consts, seq_bound)?;
     let solver = Solver::new();
 
     // Create Z3 variables for steps 0..=max_depth
@@ -54,6 +55,8 @@ pub fn check_bmc(
                 next_step: k,
                 params: &[],
                 locals: Vec::new(),
+                compound_locals: Vec::new(),
+                set_locals: Vec::new(),
             };
 
             let inv_encoded = enc.encode_bool(&inv.body)?;