diff --git a/specl/crates/specl-symbolic/src/bmc.rs b/specl/crates/specl-symbolic/src/bmc.rs index 15b66eb..cac1897 100644 --- a/specl/crates/specl-symbolic/src/bmc.rs +++ b/specl/crates/specl-symbolic/src/bmc.rs @@ -57,6 +57,7 @@ pub fn check_bmc( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_encoded = enc.encode_bool(&inv.body)?; diff --git a/specl/crates/specl-symbolic/src/encoder.rs b/specl/crates/specl-symbolic/src/encoder.rs index 06a5fba..ea9f969 100644 --- a/specl/crates/specl-symbolic/src/encoder.rs +++ b/specl/crates/specl-symbolic/src/encoder.rs @@ -27,6 +27,9 @@ pub struct EncoderCtx<'a> { /// Set locals: maps absolute locals stack position → concrete set members. /// Used for powerset quantifier bindings where the local represents a concrete subset. pub set_locals: Vec<(usize, Vec)>, + /// Whole-var locals: locals that alias an entire compound variable. + /// Each entry: (abs_depth, var_idx, step). + pub whole_var_locals: Vec<(usize, usize, usize)>, } impl<'a> EncoderCtx<'a> { @@ -136,6 +139,27 @@ impl<'a> EncoderCtx<'a> { self.compound_locals.pop(); self.locals.pop(); result + } else if let CompiledExpr::Var(var_idx) + | CompiledExpr::PrimedVar(var_idx) = value.as_ref() + { + // Bare compound variable alias (e.g., inlined function arg) + let step = if matches!(value.as_ref(), CompiledExpr::Var(_)) { + self.current_step + } else { + self.next_step + }; + let entry = &self.layout.entries[*var_idx]; + if entry.kind.z3_var_count() > 1 { + let abs_depth = self.locals.len(); + self.locals.push(Dynamic::from_ast(&Int::from_i64(0))); + self.whole_var_locals.push((abs_depth, *var_idx, step)); + let result = self.encode(body); + self.whole_var_locals.pop(); + self.locals.pop(); + return result; + } + // Re-raise the original error + self.encode(value).and_then(|_| unreachable!()) } else { // Re-raise the original error self.encode(value).and_then(|_| unreachable!()) @@ -547,10 +571,13 @@ impl<'a> EncoderCtx<'a> { domain: &CompiledExpr, predicate: &CompiledExpr, ) -> SymbolicResult { - let (lo, hi) = self.extract_range(domain)?; - // Build ITE chain: if P(lo) then lo else if P(lo+1) then lo+1 else ... else lo - let mut result = Dynamic::from_ast(&Int::from_i64(lo)); // default fallback - for val in (lo..=hi).rev() { + let values = self.resolve_domain_values(domain)?; + // Build ITE chain: if P(first) then first else if P(second) then second else ... else first + let fallback = *values + .first() + .ok_or_else(|| SymbolicError::Encoding("empty domain in choose".into()))?; + let mut result = Dynamic::from_ast(&Int::from_i64(fallback)); + for val in values.into_iter().rev() { let z3_val = Dynamic::from_ast(&Int::from_i64(val)); self.locals.push(z3_val); let pred = self.encode_bool(predicate)?; @@ -589,6 +616,12 @@ impl<'a> EncoderCtx<'a> { { return self.encode_compound_local_chain(var_idx, step, &key_z3, &keys); } + // Whole-var alias: redirect to the original compound variable + if let Some((var_idx, step)) = self.resolve_whole_var_local(*local_idx) { + let entry = &self.layout.entries[var_idx]; + let z3_vars = &self.step_vars[step][var_idx]; + return self.resolve_index_chain(&entry.kind, z3_vars, &keys); + } } let (specl_var_idx, step) = self.extract_var_step(current)?; @@ -855,12 +888,12 @@ impl<'a> EncoderCtx<'a> { filter, } = inner { - let (lo, hi) = self.extract_range(domain)?; + let values = self.resolve_domain_values(domain)?; let one = Int::from_i64(1); let zero = Int::from_i64(0); let mut sum_terms = Vec::new(); - for val in lo..=hi { + for val in values { let z3_val = Dynamic::from_ast(&Int::from_i64(val)); self.locals.push(z3_val); let included = if let Some(f) = filter { @@ -872,7 +905,11 @@ impl<'a> EncoderCtx<'a> { sum_terms.push(included.ite(&one, &zero)); } - Ok(Dynamic::from_ast(&Int::add(&sum_terms))) + if sum_terms.is_empty() { + Ok(Dynamic::from_ast(&Int::from_i64(0))) + } else { + Ok(Dynamic::from_ast(&Int::add(&sum_terms))) + } } else { match inner { CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => { @@ -1043,11 +1080,18 @@ impl<'a> EncoderCtx<'a> { domain, filter, } => { - let (lo, hi) = self.extract_range(domain)?; + let values = self.resolve_domain_values(domain)?; let elem_z3 = self.encode_int(elem)?; - let lo_z3 = Int::from_i64(lo); - let hi_z3 = Int::from_i64(hi); - let in_domain = Bool::and(&[elem_z3.ge(&lo_z3), elem_z3.le(&hi_z3)]); + let eqs: Vec = values + .iter() + .map(|v| elem_z3.eq(&Int::from_i64(*v))) + .collect(); + let eq_refs: Vec<&Bool> = eqs.iter().collect(); + let in_domain = if eq_refs.is_empty() { + Bool::from_bool(false) + } else { + Bool::or(&eq_refs) + }; let result = if let Some(f) = filter { let elem_encoded = self.encode(elem)?; @@ -1354,6 +1398,18 @@ impl<'a> EncoderCtx<'a> { None } + /// Check if a Local(idx) resolves to a whole-variable alias. + /// Returns (var_idx, step) if so. + fn resolve_whole_var_local(&self, local_idx: usize) -> Option<(usize, usize)> { + let abs_idx = self.locals.len() - 1 - local_idx; + for &(abs_depth, var_idx, step) in self.whole_var_locals.iter().rev() { + if abs_depth == abs_idx { + return Some((var_idx, step)); + } + } + None + } + /// Resolve nested len for a compound local: len(Local(n)[k1][k2]...). fn encode_compound_local_nested_len( &mut self, @@ -1677,9 +1733,9 @@ impl<'a> EncoderCtx<'a> { domain, filter, } => { - let (dom_lo, dom_hi) = self.extract_range(domain)?; + let values = self.resolve_domain_values(domain)?; let mut flags = vec![Bool::from_bool(false); count]; - for val in dom_lo..=dom_hi { + for val in values { let offset = (val - lo) as usize; if offset >= count { continue; @@ -1764,6 +1820,17 @@ impl<'a> EncoderCtx<'a> { } } + /// Resolve a domain to concrete values, handling both Range and set-local domains. + fn resolve_domain_values(&mut self, domain: &CompiledExpr) -> SymbolicResult> { + if let CompiledExpr::Local(idx) = domain { + if let Some(members) = self.resolve_set_local(*idx) { + return Ok(members.clone()); + } + } + let (lo, hi) = self.extract_range(domain)?; + Ok((lo..=hi).collect()) + } + pub fn extract_range(&mut self, domain: &CompiledExpr) -> SymbolicResult<(i64, i64)> { match domain { CompiledExpr::Range { lo, hi } => { diff --git a/specl/crates/specl-symbolic/src/ic3.rs b/specl/crates/specl-symbolic/src/ic3.rs index 3cabb8f..b9db227 100644 --- a/specl/crates/specl-symbolic/src/ic3.rs +++ b/specl/crates/specl-symbolic/src/ic3.rs @@ -98,6 +98,7 @@ pub fn check_ic3( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_encoded = enc.encode_bool(&inv.body)?; let inv_raw = inv_encoded.get_z3_ast(); diff --git a/specl/crates/specl-symbolic/src/inductive.rs b/specl/crates/specl-symbolic/src/inductive.rs index b42bdf4..9cd12fb 100644 --- a/specl/crates/specl-symbolic/src/inductive.rs +++ b/specl/crates/specl-symbolic/src/inductive.rs @@ -50,6 +50,7 @@ pub fn check_inductive( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_at_0 = enc0.encode_bool(&inv.body)?; solver.assert(&inv_at_0); @@ -64,6 +65,7 @@ pub fn check_inductive( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_at_1 = enc1.encode_bool(&inv.body)?; solver.assert(&inv_at_1.not()); diff --git a/specl/crates/specl-symbolic/src/k_induction.rs b/specl/crates/specl-symbolic/src/k_induction.rs index e0fff51..8192bb6 100644 --- a/specl/crates/specl-symbolic/src/k_induction.rs +++ b/specl/crates/specl-symbolic/src/k_induction.rs @@ -78,6 +78,7 @@ fn check_base_case( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_encoded = enc.encode_bool(&inv.body)?; solver.assert(&inv_encoded.not()); @@ -151,6 +152,7 @@ fn check_inductive_step( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_at_step = enc.encode_bool(&inv.body)?; solver.assert(&inv_at_step); @@ -167,6 +169,7 @@ fn check_inductive_step( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let inv_at_k = enc_k.encode_bool(&inv.body)?; solver.assert(&inv_at_k.not()); diff --git a/specl/crates/specl-symbolic/src/trace.rs b/specl/crates/specl-symbolic/src/trace.rs index 5165404..7c4f8d9 100644 --- a/specl/crates/specl-symbolic/src/trace.rs +++ b/specl/crates/specl-symbolic/src/trace.rs @@ -122,6 +122,7 @@ fn guard_satisfied( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let Ok(guard) = enc.encode_bool(&action.guard) else { diff --git a/specl/crates/specl-symbolic/src/transition.rs b/specl/crates/specl-symbolic/src/transition.rs index 3594ae9..46e6bf5 100644 --- a/specl/crates/specl-symbolic/src/transition.rs +++ b/specl/crates/specl-symbolic/src/transition.rs @@ -68,6 +68,7 @@ fn encode_init_expr( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let constraint = enc.encode_bool(expr)?; solver.assert(&constraint); @@ -90,6 +91,7 @@ fn encode_init_expr( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let constraint = enc.encode_bool(expr)?; solver.assert(&constraint); @@ -121,6 +123,7 @@ fn encode_init_assignment( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let rhs_z3 = enc.encode(rhs)?; if let (Some(vi), Some(ri)) = (z3_vars[0].as_int(), rhs_z3.as_int()) { @@ -151,6 +154,7 @@ fn encode_init_assignment( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let k_val = Dynamic::from_ast(&Int::from_i64(k)); enc.locals.push(k_val); @@ -188,6 +192,7 @@ fn encode_init_assignment( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let key_val = enc.extract_concrete_int_helper(key_expr)?; let offset = (key_val - key_lo) as usize; @@ -219,6 +224,7 @@ fn encode_init_assignment( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let flags = enc.encode_as_set(rhs, *lo, *hi)?; for (i, flag) in flags.iter().enumerate() { @@ -238,6 +244,7 @@ fn encode_init_assignment( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; match rhs { CompiledExpr::SeqLit(elems) => { @@ -437,6 +444,7 @@ fn encode_action( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let guard = enc.encode_bool(&action.guard)?; @@ -465,6 +473,7 @@ fn encode_action( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; let guard = enc.encode_bool(&action.guard)?; @@ -514,6 +523,7 @@ fn encode_effect( locals: Vec::new(), compound_locals: Vec::new(), set_locals: Vec::new(), + whole_var_locals: Vec::new(), }; encode_effect_expr(&action.effect, &mut enc, layout, step_vars, step) diff --git a/specl/crates/specl-syntax/src/parser.rs b/specl/crates/specl-syntax/src/parser.rs index f7448e2..8e2f3c7 100644 --- a/specl/crates/specl-syntax/src/parser.rs +++ b/specl/crates/specl-syntax/src/parser.rs @@ -618,8 +618,12 @@ impl Parser { }, span, ); - } else if self.match_token(TokenKind::LParen) { - // Function call + } else if self.check(TokenKind::LParen) + && matches!(expr.kind, ExprKind::Ident(_) | ExprKind::Field { .. }) + { + // Function call — only after identifiers and field accesses. + // Without this guard, `10\n(x = x+1)` would parse as `10(x = x+1)`. + self.advance(); let args = self.parse_call_args()?; self.expect(TokenKind::RParen)?; let span = expr.span.merge(self.prev_span());