@@ -23,18 +23,34 @@ pub(crate) use builtins::register_builtins;
2323/// Shared reference to a stats rewrite rule.
2424pub ( crate ) type StatsRewriteRuleRef = Arc < dyn StatsRewriteRule > ;
2525
26- /// A plugin-provided rule that rewrites predicates into stats-backed proof expressions .
26+ /// A plugin-provided rule for predicates whose root scalar function matches this rule .
2727///
28- /// A falsifier evaluates to `true` only when the original predicate is definitely false for the
29- /// current stats scope. A satisfier evaluates to `true` only when the original predicate is
30- /// definitely true for the current stats scope. Returning `None` means the rule cannot prove
31- /// anything for the expression.
32- #[ allow( dead_code) ]
28+ /// Rules do not produce expressions equivalent to `expr`. They produce optional sufficient
29+ /// conditions over stats for the current scope:
30+ ///
31+ /// - a falsifier evaluating to `true` proves that `expr` is false for every row in the scope;
32+ /// - a satisfier evaluating to `true` proves that `expr` is true for every row in the scope.
33+ ///
34+ /// Returning `None` means this rule cannot prove anything for the expression. A returned proof
35+ /// expression that evaluates to `false` or `null` is also inconclusive.
36+ ///
37+ /// Multiple rules may be registered for the same scalar function. Their proofs are combined with
38+ /// `OR`, so every proof returned by an individual rule must be sound on its own.
39+ ///
40+ /// `expr` is the full predicate expression whose root scalar function id is
41+ /// [`Self::scalar_fn_id`]. Use [`StatsRewriteCtx`] to resolve dtypes and recursively rewrite child
42+ /// predicates.
3343pub ( crate ) trait StatsRewriteRule : Debug + Send + Sync + ' static {
34- /// The scalar function ID this rule applies to .
44+ /// Returns the scalar function id handled by this rule .
3545 fn scalar_fn_id ( & self ) -> ScalarFnId ;
3646
37- /// Rewrite an expression into a stats-backed falsifier.
47+ /// Returns a stats-backed proof that `expr` is false for the current scope.
48+ ///
49+ /// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
50+ /// guaranteed to be false for every row in that scope. A returned proof expression that
51+ /// evaluates to `false` or `null` is inconclusive.
52+ ///
53+ /// Returns `Ok(None)` when this rule cannot construct a sound falsity proof for `expr`.
3854 fn falsify (
3955 & self ,
4056 expr : & Expression ,
@@ -45,7 +61,16 @@ pub(crate) trait StatsRewriteRule: Debug + Send + Sync + 'static {
4561 Ok ( None )
4662 }
4763
48- /// Rewrite an expression into a stats-backed satisfier.
64+ /// Returns a stats-backed proof that `expr` is true for the current scope.
65+ ///
66+ /// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
67+ /// guaranteed to be true for every row in that scope. A returned proof expression that
68+ /// evaluates to `false` or `null` is inconclusive.
69+ ///
70+ /// This is not the complement of [`Self::falsify`]; both methods are one-way proofs and may be
71+ /// implemented independently.
72+ ///
73+ /// Returns `Ok(None)` when this rule cannot construct a sound truth proof for `expr`.
4974 fn satisfy (
5075 & self ,
5176 expr : & Expression ,
0 commit comments