From 539b0fc1316ee03a9820d52a83ad8af669636add Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 30 Dec 2025 11:48:56 +0900 Subject: [PATCH 1/2] Enable to add guard to Atom --- src/chc.rs | 77 ++++++++++++++++++++++++++++++++++++++-------- src/chc/smtlib2.rs | 7 +++++ src/chc/unbox.rs | 5 +-- 3 files changed, 74 insertions(+), 15 deletions(-) diff --git a/src/chc.rs b/src/chc.rs index a5f046e..a2c4b30 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -997,6 +997,12 @@ impl Pred { /// An atom is a predicate applied to a list of terms. #[derive(Debug, Clone)] pub struct Atom { + /// With `guard`, this represents `guard => pred(args)`. + /// + /// As long as there is no pvar in the `guard`, it forms a valid CHC. However, in that case, + /// it becomes odd to call this an `Atom`... It is our TODO to clean this up by either + /// getting rid of the `guard` or renaming `Atom`. + pub guard: Option>>, pub pred: Pred, pub args: Vec>, } @@ -1008,7 +1014,12 @@ where D::Doc: Clone, { fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - if self.pred.is_infix() { + let guard = if let Some(guard) = &self.guard { + guard.pretty(allocator).append(allocator.text(" ⇒")) + } else { + allocator.nil() + }; + let atom = if self.pred.is_infix() { self.args[0] .pretty_atom(allocator) .append(allocator.line()) @@ -1027,35 +1038,50 @@ where } else { p.append(allocator.line()).append(inner.nest(2)).group() } - } + }; + guard.append(allocator.line()).append(atom).group() } } impl Atom { pub fn new(pred: Pred, args: Vec>) -> Self { - Atom { pred, args } + Atom { + guard: None, + pred, + args, + } } - pub fn top() -> Self { + pub fn with_guard(guard: Formula, pred: Pred, args: Vec>) -> Self { Atom { - pred: KnownPred::TOP.into(), - args: vec![], + guard: Some(Box::new(guard)), + pred, + args, } } + pub fn top() -> Self { + Atom::new(KnownPred::TOP.into(), vec![]) + } + pub fn bottom() -> Self { - Atom { - pred: KnownPred::BOTTOM.into(), - args: vec![], - } + Atom::new(KnownPred::BOTTOM.into(), vec![]) } pub fn is_top(&self) -> bool { - self.pred.is_top() + if let Some(guard) = &self.guard { + guard.is_bottom() || self.pred.is_top() + } else { + self.pred.is_top() + } } pub fn is_bottom(&self) -> bool { - self.pred.is_bottom() + if let Some(guard) = &self.guard { + guard.is_top() && self.pred.is_bottom() + } else { + self.pred.is_bottom() + } } pub fn subst_var(self, mut f: F) -> Atom @@ -1063,6 +1089,7 @@ impl Atom { F: FnMut(V) -> Term, { Atom { + guard: self.guard.map(|fo| Box::new(fo.subst_var(&mut f))), pred: self.pred, args: self.args.into_iter().map(|t| t.subst_var(&mut f)).collect(), } @@ -1073,13 +1100,37 @@ impl Atom { F: FnMut(V) -> W, { Atom { + guard: self.guard.map(|fo| Box::new(fo.map_var(&mut f))), pred: self.pred, args: self.args.into_iter().map(|t| t.map_var(&mut f)).collect(), } } pub fn fv(&self) -> impl Iterator { - self.args.iter().flat_map(|t| t.fv()) + let guard_fvs: Box> = if let Some(guard) = &self.guard { + Box::new(guard.fv()) + } else { + Box::new(std::iter::empty()) + }; + self.args.iter().flat_map(|t| t.fv()).chain(guard_fvs) + } + + pub fn guarded(self, new_guard: Formula) -> Atom { + let Atom { + guard: self_guard, + pred, + args, + } = self; + let guard = if let Some(self_guard) = self_guard { + self_guard.and(new_guard) + } else { + new_guard + }; + Atom { + guard: Some(Box::new(guard)), + pred, + args, + } } } diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs index 3cef75e..167d108 100644 --- a/src/chc/smtlib2.rs +++ b/src/chc/smtlib2.rs @@ -223,6 +223,10 @@ pub struct Atom<'ctx, 'a> { impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + if let Some(guard) = &self.inner.guard { + let guard = Formula::new(self.ctx, self.clause, guard); + write!(f, "(=> {} ", guard)?; + } if self.inner.pred.is_negative() { write!(f, "(not ")?; } @@ -244,6 +248,9 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> { if self.inner.pred.is_negative() { write!(f, ")")?; } + if self.inner.guard.is_some() { + write!(f, ")")?; + } Ok(()) } } diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index ffc4600..667ab39 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -24,9 +24,10 @@ fn unbox_term(term: Term) -> Term { } fn unbox_atom(atom: Atom) -> Atom { - let Atom { pred, args } = atom; + let Atom { guard, pred, args } = atom; + let guard = guard.map(|fo| Box::new(unbox_formula(*fo))); let args = args.into_iter().map(unbox_term).collect(); - Atom { pred, args } + Atom { guard, pred, args } } fn unbox_datatype_sort(sort: DatatypeSort) -> DatatypeSort { From 750b03a0c858eebee71155fe746d872b455b9205 Mon Sep 17 00:00:00 2001 From: coord_e Date: Tue, 30 Dec 2025 12:46:28 +0900 Subject: [PATCH 2/2] Add guard of discriminant when expanding variant field types --- src/chc.rs | 16 +++++++++++++++ src/refine/env.rs | 18 +++++++++++------ src/rty.rs | 22 +++++++++++++++++++++ tests/ui/fail/adt_variant_without_params.rs | 13 ++++++++++++ tests/ui/pass/adt_variant_without_params.rs | 13 ++++++++++++ 5 files changed, 76 insertions(+), 6 deletions(-) create mode 100644 tests/ui/fail/adt_variant_without_params.rs create mode 100644 tests/ui/pass/adt_variant_without_params.rs diff --git a/src/chc.rs b/src/chc.rs index a2c4b30..5543de4 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1507,6 +1507,22 @@ impl Body { } } +impl Body +where + V: Var, +{ + pub fn guarded(self, guard: Formula) -> Body { + let Body { atoms, formula } = self; + Body { + atoms: atoms + .into_iter() + .map(|a| a.guarded(guard.clone())) + .collect(), + formula: guard.not().or(formula), + } + } +} + impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Body where V: Var, diff --git a/src/refine/env.rs b/src/refine/env.rs index f18dadb..3663d81 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -730,6 +730,12 @@ impl Env { let def = self.enum_defs[&ty.symbol].clone(); let matcher_pred = chc::MatcherPred::new(ty.symbol.clone(), ty.arg_sorts()); + let discr_var = self + .temp_vars + .push(TempVarBinding::Type(rty::RefinedType::unrefined( + rty::Type::int(), + ))); + let mut variants = IndexVec::new(); for variant_def in &def.variants { let mut fields = IndexVec::new(); @@ -738,7 +744,12 @@ impl Env { fields.push(x); let mut field_ty = rty::RefinedType::unrefined(field_ty.clone().vacuous()); field_ty.instantiate_ty_params(ty.args.clone()); - self.bind_impl(x.into(), field_ty.boxed(), depth); + let guarded_field_ty = field_ty.guarded( + chc::Term::var(discr_var.into()) + .equal_to(chc::Term::int(variant_def.discr as i64)) + .into(), + ); + self.bind_impl(x.into(), guarded_field_ty.boxed(), depth); } variants.push(FlowBindingVariant { fields }); } @@ -773,11 +784,6 @@ impl Env { assumption .body .push_conj(chc::Atom::new(matcher_pred.into(), pred_args)); - let discr_var = self - .temp_vars - .push(TempVarBinding::Type(rty::RefinedType::unrefined( - rty::Type::int(), - ))); assumption .body .push_conj( diff --git a/src/rty.rs b/src/rty.rs index 34cfd6d..4c3d2a1 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1172,6 +1172,19 @@ impl Formula { } } +impl Formula +where + V: chc::Var, +{ + pub fn guarded(self, guard: chc::Formula) -> Self { + let Formula { existentials, body } = self; + Formula { + existentials, + body: body.guarded(guard), + } + } +} + impl Formula where V: ShiftExistential, @@ -1351,6 +1364,15 @@ impl RefinedType { RefinedType { ty, refinement } } + pub fn guarded(self, guard: chc::Formula) -> Self + where + FV: chc::Var, + { + let RefinedType { ty, refinement } = self; + let refinement = refinement.guarded(guard.map_var(RefinedTypeVar::Free)); + RefinedType { ty, refinement } + } + /// Returns a dereferenced type of the immutable reference or owned pointer. /// /// e.g. `{ v: Box | φ } --> { v: T | φ[box v/v] }` diff --git a/tests/ui/fail/adt_variant_without_params.rs b/tests/ui/fail/adt_variant_without_params.rs new file mode 100644 index 0000000..bd8c500 --- /dev/null +++ b/tests/ui/fail/adt_variant_without_params.rs @@ -0,0 +1,13 @@ +//@error-in-other-file: Unsat + +enum X { + None1, + None2, + Some(T), +} + +fn main() { + let mut opt: X = X::None1; + opt = X::None2; + assert!(matches!(opt, X::None1)); +} diff --git a/tests/ui/pass/adt_variant_without_params.rs b/tests/ui/pass/adt_variant_without_params.rs new file mode 100644 index 0000000..15bd1e4 --- /dev/null +++ b/tests/ui/pass/adt_variant_without_params.rs @@ -0,0 +1,13 @@ +//@check-pass + +enum X { + None1, + None2, + Some(T), +} + +fn main() { + let mut opt: X = X::None1; + opt = X::None2; + assert!(matches!(opt, X::None2)); +}