From e078fe1dc36c92ee35cc2cdc9ba638adf0e12da4 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 25 Dec 2025 08:24:37 +0000 Subject: [PATCH 01/15] add: test for annotations of predicates --- tests/ui/pass/annot_preds.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/ui/pass/annot_preds.rs diff --git a/tests/ui/pass/annot_preds.rs b/tests/ui/pass/annot_preds.rs new file mode 100644 index 0000000..79bf978 --- /dev/null +++ b/tests/ui/pass/annot_preds.rs @@ -0,0 +1,24 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +#[thrust::predicate] +fn is_double(x: i64, doubled_x: i64) -> bool { + x * 2 == doubled_x + // "(=( + // (* (x 2)) + // doubled_x + // ))" +} + +#[thrust::requires(true)] +#[thrust::ensures(result == 2 * x)] +// #[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +fn main() { + let a = 3; + assert!(double(a) == 6); + assert!(is_double(a, double(a))); +} From 5922d4f1288afb828a957456a5b536f5bffb000b Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 16:10:37 +0900 Subject: [PATCH 02/15] Merge main --- src/analyze/local_def.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index d556ef0..61cb80d 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -135,7 +135,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .next() .is_some() } - + // TODO: unify this logic with extraction functions above pub fn is_fully_annotated(&self) -> bool { let has_require = self From e413cd0b1b2af35c1b35b5c662ca7a2d8b55437a Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 9 Jan 2026 05:58:01 +0000 Subject: [PATCH 03/15] add: definition for user-defined predicates in CHC --- src/chc.rs | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/src/chc.rs b/src/chc.rs index 67ef92b..72873be 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -902,12 +902,87 @@ impl MatcherPred { } } +// TODO: DatatypeSymbolをほぼそのままコピーする形になっているので、エイリアスなどで共通化すべき？ +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub struct UserDefinedPredSymbol { + inner: String, +} + +impl std::fmt::Display for UserDefinedPredSymbol { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + self.inner.fmt(f) + } +} + +impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPredSymbol +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + allocator.text(self.inner.clone()) + } +} + +impl UserDefinedPredSymbol { + pub fn new(inner: String) -> Self { + Self { inner } + } +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub struct UserDefinedPred { + symbol: UserDefinedPredSymbol, + args: Vec, +} + +impl<'a> std::fmt::Display for UserDefinedPred { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + write!(f, "{}", self.symbol.inner) + } +} + +impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPred +where + D: pretty::DocAllocator<'a, termcolor::ColorSpec>, + D::Doc: Clone, +{ + fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { + let args = allocator.intersperse( + self.args.iter().map(|a| a.pretty(allocator)), + allocator.text(", "), + ); + allocator + .text("user_defined_pred") + .append( + allocator + .text(self.symbol.inner.clone()) + .append(args.angles()) + .angles(), + ) + .group() + } +} + +impl UserDefinedPred { + pub fn new(symbol: UserDefinedPredSymbol, args: Vec) -> Self { + Self { + symbol, + args, + } + } + + pub fn name(&self) -> &str { + &self.symbol.inner + } +} + /// A predicate. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Pred { Known(KnownPred), Var(PredVarId), Matcher(MatcherPred), + UserDefined(UserDefinedPredSymbol), } impl std::fmt::Display for Pred { @@ -916,6 +991,7 @@ impl std::fmt::Display for Pred { Pred::Known(p) => p.fmt(f), Pred::Var(p) => p.fmt(f), Pred::Matcher(p) => p.fmt(f), + Pred::UserDefined(p) => p.fmt(f), } } } @@ -930,6 +1006,7 @@ where Pred::Known(p) => p.pretty(allocator), Pred::Var(p) => p.pretty(allocator), Pred::Matcher(p) => p.pretty(allocator), + Pred::UserDefined(p) => p.pretty(allocator), } } } @@ -958,6 +1035,7 @@ impl Pred { Pred::Known(p) => p.name().into(), Pred::Var(p) => p.to_string().into(), Pred::Matcher(p) => p.name().into(), + Pred::UserDefined(p) => p.inner.clone().into(), } } @@ -966,6 +1044,7 @@ impl Pred { Pred::Known(p) => p.is_negative(), Pred::Var(_) => false, Pred::Matcher(_) => false, + Pred::UserDefined(_) => false, } } @@ -974,6 +1053,7 @@ impl Pred { Pred::Known(p) => p.is_infix(), Pred::Var(_) => false, Pred::Matcher(_) => false, + Pred::UserDefined(_) => false, } } @@ -982,6 +1062,7 @@ impl Pred { Pred::Known(p) => p.is_top(), Pred::Var(_) => false, Pred::Matcher(_) => false, + Pred::UserDefined(_) => false, } } @@ -990,6 +1071,7 @@ impl Pred { Pred::Known(p) => p.is_bottom(), Pred::Var(_) => false, Pred::Matcher(_) => false, + Pred::UserDefined(_) => false, } } } From dce2328f5adf11cf478ec938cee3510459502555 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Fri, 9 Jan 2026 06:17:40 +0000 Subject: [PATCH 04/15] add: an implementation for unboxing user-defined predicates --- src/chc/unbox.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs index 8ed320f..30ea31c 100644 --- a/src/chc/unbox.rs +++ b/src/chc/unbox.rs @@ -42,6 +42,7 @@ fn unbox_pred(pred: Pred) -> Pred { Pred::Known(pred) => Pred::Known(pred), Pred::Var(pred) => Pred::Var(pred), Pred::Matcher(pred) => unbox_matcher_pred(pred), + Pred::UserDefined(pred) => Pred::UserDefined(pred), } } From 1816532a4bbf57d79031bf4b5d0539c5ba45e7d3 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 17:27:05 +0900 Subject: [PATCH 05/15] add: parse single-path identifier followed by parenthesized arguments as a user-defined predicate call --- src/annot.rs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/annot.rs b/src/annot.rs index 128c289..dacf709 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -478,6 +478,17 @@ where FormulaOrTerm::Term(var, sort.clone()) } _ => { + if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, _args)) = self.look_ahead_token_tree(1) { + self.consume(); + let pred_symbol = chc::UserDefinedPredSymbol::new(ident.name.to_string()); + let pred = chc::Pred::UserDefined(pred_symbol); + + let args = self.parse_datatype_ctor_args()?; + + let atom = chc::Atom::new(pred, args); + let formula = chc::Formula::Atom(atom); + return Ok(FormulaOrTerm::Formula(formula)); + } let (v, sort) = self.resolve(*ident)?; FormulaOrTerm::Term(chc::Term::var(v), sort) } From 2b0e2bb7f78794fdee9f3d3516aad48bb7cf37e7 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 19:00:11 +0900 Subject: [PATCH 06/15] fix: wrong implementation of parser for predicate call arguments --- src/annot.rs | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/annot.rs b/src/annot.rs index dacf709..a9ec235 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -477,14 +477,23 @@ where chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string()); FormulaOrTerm::Term(var, sort.clone()) } - _ => { - if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, _args)) = self.look_ahead_token_tree(1) { + _ => { + let next_tt = self.look_ahead_token_tree(0); + + if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt { + let args = args.clone(); self.consume(); + let pred_symbol = chc::UserDefinedPredSymbol::new(ident.name.to_string()); let pred = chc::Pred::UserDefined(pred_symbol); - let args = self.parse_datatype_ctor_args()?; - + let mut parser = Parser { + resolver: self.boxed_resolver(), + cursor: args.trees(), + formula_existentials: self.formula_existentials.clone(), + }; + let args = parser.parse_datatype_ctor_args()?; + let atom = chc::Atom::new(pred, args); let formula = chc::Formula::Atom(atom); return Ok(FormulaOrTerm::Formula(formula)); From adbd61f690c5ad4ab27bf496389d0d72bad1e94f Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 19:04:55 +0900 Subject: [PATCH 07/15] change: use raw_define to define user-defined predicates for now --- tests/ui/pass/annot_preds.rs | 24 ------------------------ tests/ui/pass/annot_preds_raw_define.rs | 25 +++++++++++++++++++++++++ 2 files changed, 25 insertions(+), 24 deletions(-) delete mode 100644 tests/ui/pass/annot_preds.rs create mode 100644 tests/ui/pass/annot_preds_raw_define.rs diff --git a/tests/ui/pass/annot_preds.rs b/tests/ui/pass/annot_preds.rs deleted file mode 100644 index 79bf978..0000000 --- a/tests/ui/pass/annot_preds.rs +++ /dev/null @@ -1,24 +0,0 @@ -//@check-pass -//@compile-flags: -Adead_code -C debug-assertions=off - -#[thrust::predicate] -fn is_double(x: i64, doubled_x: i64) -> bool { - x * 2 == doubled_x - // "(=( - // (* (x 2)) - // doubled_x - // ))" -} - -#[thrust::requires(true)] -#[thrust::ensures(result == 2 * x)] -// #[thrust::ensures(is_double(x, result))] -fn double(x: i64) -> i64 { - x + x -} - -fn main() { - let a = 3; - assert!(double(a) == 6); - assert!(is_double(a, double(a))); -} diff --git a/tests/ui/pass/annot_preds_raw_define.rs b/tests/ui/pass/annot_preds_raw_define.rs new file mode 100644 index 0000000..bfcde39 --- /dev/null +++ b/tests/ui/pass/annot_preds_raw_define.rs @@ -0,0 +1,25 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +// Insert definitions written in SMT-LIB2 format into .smt file directly. +// This feature is intended for debug or experiment purpose. +#![feature(custom_inner_attributes)] +#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (= + (* x 2) + doubled_x + ) +)")] + +#[thrust::requires(true)] +// #[thrust::ensures(result == 2 * x)] +#[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +fn main() { + let a = 3; + assert!(double(a) == 6); + // assert!(is_double(a, double(a))); +} From 4758c7048a19ca130b0bf86317494b6ae7eeb007 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 19:19:18 +0900 Subject: [PATCH 08/15] fix: translate comment into English --- src/chc.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/chc.rs b/src/chc.rs index 72873be..4d12d8d 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -902,7 +902,7 @@ impl MatcherPred { } } -// TODO: DatatypeSymbolをほぼそのままコピーする形になっているので、エイリアスなどで共通化すべき？ +// TODO: This struct is almost copy of `DatatypeSymbol`. Two traits maight be unified with aliases. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct UserDefinedPredSymbol { inner: String, From 01c66cf42cb79de78d6174fc30bee30ca0e61edc Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 12 Jan 2026 20:18:13 +0900 Subject: [PATCH 09/15] add: more test for user-defined predicate calls --- tests/ui/pass/annot_preds_raw_define_multi.rs | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 tests/ui/pass/annot_preds_raw_define_multi.rs diff --git a/tests/ui/pass/annot_preds_raw_define_multi.rs b/tests/ui/pass/annot_preds_raw_define_multi.rs new file mode 100644 index 0000000..c0419f9 --- /dev/null +++ b/tests/ui/pass/annot_preds_raw_define_multi.rs @@ -0,0 +1,36 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +#![feature(custom_inner_attributes)] +#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (= + (* x 2) + doubled_x + ) +)")] + +#![thrust::raw_define("(define-fun is_triple ((x Int) (tripled_x Int)) Bool + (= + (* x 3) + tripled_x + ) +)")] + +#[thrust::requires(true)] +#[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +#[thrust::require(is_double(x, doubled_x))] +#[thrust::ensures(is_triple(x, result))] +fn triple(x: i64, doubled_x: i64) -> i64 { + x + doubled_x +} + +fn main() { + let a = 3; + let double_a = double(a); + assert!(double_a == 6); + assert!(triple(a, double_a) == 9); +} From e8a9e02f6c402d3799c6f6b1e90d1eee940e2a3a Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Wed, 14 Jan 2026 13:55:21 +0000 Subject: [PATCH 10/15] fix: reflect review comments in PR --- src/annot.rs | 10 ++++++---- src/chc.rs | 3 +-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/annot.rs b/src/annot.rs index a9ec235..5987922 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -420,7 +420,7 @@ where Ok(AnnotPath { segments }) } - fn parse_datatype_ctor_args(&mut self) -> Result>> { + fn parse_arg_terms(&mut self) -> Result>> { if self.look_ahead_token(0).is_none() { return Ok(Vec::new()); } @@ -477,7 +477,9 @@ where chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string()); FormulaOrTerm::Term(var, sort.clone()) } - _ => { + _ => { + // If the single-segment identifier is followed by parethesized arguments, + // parse them as user-defined predicate calls. let next_tt = self.look_ahead_token_tree(0); if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt { @@ -492,7 +494,7 @@ where cursor: args.trees(), formula_existentials: self.formula_existentials.clone(), }; - let args = parser.parse_datatype_ctor_args()?; + let args = parser.parse_arg_terms()?; let atom = chc::Atom::new(pred, args); let formula = chc::Formula::Atom(atom); @@ -517,7 +519,7 @@ where cursor: s.trees(), formula_existentials: self.formula_existentials.clone(), }; - let args = parser.parse_datatype_ctor_args()?; + let args = parser.parse_arg_terms()?; parser.end_of_input()?; let (term, sort) = path.to_datatype_ctor(args); FormulaOrTerm::Term(term, sort) diff --git a/src/chc.rs b/src/chc.rs index 4d12d8d..a2c4c23 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -902,7 +902,6 @@ impl MatcherPred { } } -// TODO: This struct is almost copy of `DatatypeSymbol`. Two traits maight be unified with aliases. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct UserDefinedPredSymbol { inner: String, @@ -1035,7 +1034,7 @@ impl Pred { Pred::Known(p) => p.name().into(), Pred::Var(p) => p.to_string().into(), Pred::Matcher(p) => p.name().into(), - Pred::UserDefined(p) => p.inner.clone().into(), + Pred::UserDefined(p) => p.to_string().into(), } } From ee1f6e97082c315b546b7bb5e7c7add36b416735 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Thu, 15 Jan 2026 09:29:38 +0000 Subject: [PATCH 11/15] change: delete `UserDefinedPred` and rename `UserDefinedPredSymbol` to `UserDefinedPred` --- src/annot.rs | 2 +- src/chc.rs | 57 +++++----------------------------------------------- 2 files changed, 6 insertions(+), 53 deletions(-) diff --git a/src/annot.rs b/src/annot.rs index 5987922..a637fcc 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -486,7 +486,7 @@ where let args = args.clone(); self.consume(); - let pred_symbol = chc::UserDefinedPredSymbol::new(ident.name.to_string()); + let pred_symbol = chc::UserDefinedPred::new(ident.name.to_string()); let pred = chc::Pred::UserDefined(pred_symbol); let mut parser = Parser { diff --git a/src/chc.rs b/src/chc.rs index a2c4c23..a35f12c 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -903,17 +903,17 @@ impl MatcherPred { } #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub struct UserDefinedPredSymbol { +pub struct UserDefinedPred { inner: String, } -impl std::fmt::Display for UserDefinedPredSymbol { +impl std::fmt::Display for UserDefinedPred { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { self.inner.fmt(f) } } -impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPredSymbol +impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPred where D: pretty::DocAllocator<'a, termcolor::ColorSpec>, { @@ -922,66 +922,19 @@ where } } -impl UserDefinedPredSymbol { +impl UserDefinedPred { pub fn new(inner: String) -> Self { Self { inner } } } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub struct UserDefinedPred { - symbol: UserDefinedPredSymbol, - args: Vec, -} - -impl<'a> std::fmt::Display for UserDefinedPred { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(f, "{}", self.symbol.inner) - } -} - -impl<'a, 'b, D> Pretty<'a, D, termcolor::ColorSpec> for &'b UserDefinedPred -where - D: pretty::DocAllocator<'a, termcolor::ColorSpec>, - D::Doc: Clone, -{ - fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> { - let args = allocator.intersperse( - self.args.iter().map(|a| a.pretty(allocator)), - allocator.text(", "), - ); - allocator - .text("user_defined_pred") - .append( - allocator - .text(self.symbol.inner.clone()) - .append(args.angles()) - .angles(), - ) - .group() - } -} - -impl UserDefinedPred { - pub fn new(symbol: UserDefinedPredSymbol, args: Vec) -> Self { - Self { - symbol, - args, - } - } - - pub fn name(&self) -> &str { - &self.symbol.inner - } -} - /// A predicate. #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Pred { Known(KnownPred), Var(PredVarId), Matcher(MatcherPred), - UserDefined(UserDefinedPredSymbol), + UserDefined(UserDefinedPred), } impl std::fmt::Display for Pred { From 5d1e6d9f792309bd007cdf680e15d1b9b29091e3 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 20 Jan 2026 23:04:30 +0900 Subject: [PATCH 12/15] remove: accidentally duplicated negative tests --- tests/ui/pass/annot_preds_raw_define.rs | 25 ------------- tests/ui/pass/annot_preds_raw_define_multi.rs | 36 ------------------- 2 files changed, 61 deletions(-) delete mode 100644 tests/ui/pass/annot_preds_raw_define.rs delete mode 100644 tests/ui/pass/annot_preds_raw_define_multi.rs diff --git a/tests/ui/pass/annot_preds_raw_define.rs b/tests/ui/pass/annot_preds_raw_define.rs deleted file mode 100644 index bfcde39..0000000 --- a/tests/ui/pass/annot_preds_raw_define.rs +++ /dev/null @@ -1,25 +0,0 @@ -//@check-pass -//@compile-flags: -Adead_code -C debug-assertions=off - -// Insert definitions written in SMT-LIB2 format into .smt file directly. -// This feature is intended for debug or experiment purpose. -#![feature(custom_inner_attributes)] -#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool - (= - (* x 2) - doubled_x - ) -)")] - -#[thrust::requires(true)] -// #[thrust::ensures(result == 2 * x)] -#[thrust::ensures(is_double(x, result))] -fn double(x: i64) -> i64 { - x + x -} - -fn main() { - let a = 3; - assert!(double(a) == 6); - // assert!(is_double(a, double(a))); -} diff --git a/tests/ui/pass/annot_preds_raw_define_multi.rs b/tests/ui/pass/annot_preds_raw_define_multi.rs deleted file mode 100644 index c0419f9..0000000 --- a/tests/ui/pass/annot_preds_raw_define_multi.rs +++ /dev/null @@ -1,36 +0,0 @@ -//@check-pass -//@compile-flags: -Adead_code -C debug-assertions=off - -#![feature(custom_inner_attributes)] -#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool - (= - (* x 2) - doubled_x - ) -)")] - -#![thrust::raw_define("(define-fun is_triple ((x Int) (tripled_x Int)) Bool - (= - (* x 3) - tripled_x - ) -)")] - -#[thrust::requires(true)] -#[thrust::ensures(is_double(x, result))] -fn double(x: i64) -> i64 { - x + x -} - -#[thrust::require(is_double(x, doubled_x))] -#[thrust::ensures(is_triple(x, result))] -fn triple(x: i64, doubled_x: i64) -> i64 { - x + doubled_x -} - -fn main() { - let a = 3; - let double_a = double(a); - assert!(double_a == 6); - assert!(triple(a, double_a) == 9); -} From 463e7d3168efe6e4709bd98cb69900edf1f749cf Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Mon, 19 Jan 2026 07:42:36 +0000 Subject: [PATCH 13/15] fix: execute cargo clippy and fmt --- src/analyze/local_def.rs | 2 +- src/annot.rs | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 61cb80d..d556ef0 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -135,7 +135,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { .next() .is_some() } - + // TODO: unify this logic with extraction functions above pub fn is_fully_annotated(&self) -> bool { let has_require = self diff --git a/src/annot.rs b/src/annot.rs index a637fcc..30bf7d3 100644 --- a/src/annot.rs +++ b/src/annot.rs @@ -482,7 +482,9 @@ where // parse them as user-defined predicate calls. let next_tt = self.look_ahead_token_tree(0); - if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = next_tt { + if let Some(TokenTree::Delimited(_, _, Delimiter::Parenthesis, args)) = + next_tt + { let args = args.clone(); self.consume(); From 24869fdde55da4e1a269091017e3d33195c6ac0c Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 20 Jan 2026 15:22:54 +0000 Subject: [PATCH 14/15] add: impl From for Pred --- src/chc.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/chc.rs b/src/chc.rs index a35f12c..e9741bb 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -981,6 +981,12 @@ impl From for Pred { } } +impl From for Pred { + fn from(p: UserDefinedPred) -> Pred { + Pred::UserDefined(p) + } +} + impl Pred { pub fn name(&self) -> std::borrow::Cow<'static, str> { match self { From a91e021bf1819087a5856b86ce33b1b6c0a76219 Mon Sep 17 00:00:00 2001 From: coeff-aij <175928954+coeff-aij@users.noreply.github.com> Date: Tue, 20 Jan 2026 15:34:05 +0000 Subject: [PATCH 15/15] fix: restore tests accidentally deleted --- tests/ui/pass/annot_preds_raw_command.rs | 21 +++++++++++ .../ui/pass/annot_preds_raw_command_multi.rs | 36 +++++++++++++++++++ 2 files changed, 57 insertions(+) create mode 100644 tests/ui/pass/annot_preds_raw_command.rs create mode 100644 tests/ui/pass/annot_preds_raw_command_multi.rs diff --git a/tests/ui/pass/annot_preds_raw_command.rs b/tests/ui/pass/annot_preds_raw_command.rs new file mode 100644 index 0000000..a596c4f --- /dev/null +++ b/tests/ui/pass/annot_preds_raw_command.rs @@ -0,0 +1,21 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +#![feature(custom_inner_attributes)] +#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (= + (* x 2) + doubled_x + ) +)")] + +#[thrust::requires(true)] +#[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +fn main() { + let a = 3; + assert!(double(a) == 6); +} \ No newline at end of file diff --git a/tests/ui/pass/annot_preds_raw_command_multi.rs b/tests/ui/pass/annot_preds_raw_command_multi.rs new file mode 100644 index 0000000..0dbfb0d --- /dev/null +++ b/tests/ui/pass/annot_preds_raw_command_multi.rs @@ -0,0 +1,36 @@ +//@check-pass +//@compile-flags: -Adead_code -C debug-assertions=off + +#![feature(custom_inner_attributes)] +#![thrust::raw_command("(define-fun is_double ((x Int) (doubled_x Int)) Bool + (= + (* x 2) + doubled_x + ) +)")] + +#![thrust::raw_command("(define-fun is_triple ((x Int) (tripled_x Int)) Bool + (= + (* x 3) + tripled_x + ) +)")] + +#[thrust::requires(true)] +#[thrust::ensures(is_double(x, result))] +fn double(x: i64) -> i64 { + x + x +} + +#[thrust::require(is_double(x, doubled_x))] +#[thrust::ensures(is_triple(x, result))] +fn triple(x: i64, doubled_x: i64) -> i64 { + x + doubled_x +} + +fn main() { + let a = 3; + let double_a = double(a); + assert!(double_a == 6); + assert!(triple(a, double_a) == 9); +} \ No newline at end of file