Skip to main content

is_empty_and_conjunction

partition::utils::split

Function is_empty_and_conjunction 

Source 
fn is_empty_and_conjunction(expr: &PartitionExpr) -> bool
Expand description

Detects whether a pure conjunction expression is definitely unsatisfiable.

Scope and intent:

  • This checker is intentionally conservative.
  • It only analyzes expressions that can be flattened into: atom1 AND atom2 AND ...
  • If any OR is present, it returns false (unknown / not handled here).

Strategy:

  • For each column, keep only the tightest lower bound (> / >=) and tightest upper bound (< / <=).
  • = is treated as both lower and upper bound at the same value.
  • != is tracked per column to catch direct conflicts with =.
  • After bounds are collected, the conjunction is empty iff for any column:
    • lower value is greater than upper value, or
    • lower value equals upper value but at least one bound is exclusive.
  • For discrete domains (Int*, UInt*), adjacent open bounds with no representable value in between are also treated as empty.

Notes:

  • This is still a conservative fast path focused on conjunction emptiness detection for split degradation.
  • split_partition_expr currently restricts its main path to range-only conjunctions, but this helper remains slightly more general so shared bound collection and direct conflict checks stay reusable.