Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 34 additions & 9 deletions vortex-array/src/stats/rewrite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,18 +23,34 @@ pub(crate) use builtins::register_builtins;
/// Shared reference to a stats rewrite rule.
pub(crate) type StatsRewriteRuleRef = Arc<dyn StatsRewriteRule>;

/// A plugin-provided rule that rewrites predicates into stats-backed proof expressions.
/// A plugin-provided rule for predicates whose root scalar function matches this rule.
///
/// A falsifier evaluates to `true` only when the original predicate is definitely false for the
/// current stats scope. A satisfier evaluates to `true` only when the original predicate is
/// definitely true for the current stats scope. Returning `None` means the rule cannot prove
/// anything for the expression.
#[allow(dead_code)]
/// Rules do not produce expressions equivalent to `expr`. They produce optional sufficient
/// conditions over stats for the current scope:
///
/// - a falsifier evaluating to `true` proves that `expr` is false for every row in the scope;
/// - a satisfier evaluating to `true` proves that `expr` is true for every row in the scope.
///
/// Returning `None` means this rule cannot prove anything for the expression. A returned proof
/// expression that evaluates to `false` or `null` is also inconclusive.
///
/// Multiple rules may be registered for the same scalar function. Their proofs are combined with
/// `OR`, so every proof returned by an individual rule must be sound on its own.
///
/// `expr` is the full predicate expression whose root scalar function id is
/// [`Self::scalar_fn_id`]. Use [`StatsRewriteCtx`] to resolve dtypes and recursively rewrite child
/// predicates.
pub(crate) trait StatsRewriteRule: Debug + Send + Sync + 'static {
/// The scalar function ID this rule applies to.
/// Returns the scalar function id handled by this rule.
fn scalar_fn_id(&self) -> ScalarFnId;

/// Rewrite an expression into a stats-backed falsifier.
/// Returns a stats-backed proof that `expr` is false for the current scope.
///
/// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
/// guaranteed to be false for every row in that scope. A returned proof expression that
/// evaluates to `false` or `null` is inconclusive.
///
/// Returns `Ok(None)` when this rule cannot construct a sound falsity proof for `expr`.
fn falsify(
&self,
expr: &Expression,
Expand All @@ -45,7 +61,16 @@ pub(crate) trait StatsRewriteRule: Debug + Send + Sync + 'static {
Ok(None)
}

/// Rewrite an expression into a stats-backed satisfier.
/// Returns a stats-backed proof that `expr` is true for the current scope.
///
/// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
/// guaranteed to be true for every row in that scope. A returned proof expression that
/// evaluates to `false` or `null` is inconclusive.
///
/// This is not the complement of [`Self::falsify`]; both methods are one-way proofs and may be
/// implemented independently.
///
/// Returns `Ok(None)` when this rule cannot construct a sound truth proof for `expr`.
fn satisfy(
&self,
expr: &Expression,
Expand Down
Loading