Optimization¶

The optimizer applies rules to simplify expressions and detect logical issues.

Basic Examples¶

from therismos import optimize, F, TRUE, FALSE, AllExpr, AnyExpr

age = F("age")

# Identity elimination
expr = AllExpr(age > 18, TRUE, age < 65)
result, _ = optimize(expr)
# result: AllExpr(age > 18, age < 65)

# Contradiction detection
expr = (age == 25) & (age != 25)
result, _ = optimize(expr)
# result: FALSE

# Tautology detection
expr = (age < 30) | (age >= 30)
result, _ = optimize(expr)
# result: TRUE

# NOT simplification (De Morgan's laws)
name = F("name")
expr = ~((age > 18) & (name == "Alice"))
result, _ = optimize(expr)
# result: (age <= 18) OR (name != "Alice")

Optimization Rules Reference¶

Atomic Expression Simplifications¶

Rule	Before	After
Empty IN to FALSE	`f IN ()`	`FALSE`
Single-value IN to Eq	`f IN (v)`	`f == v`
Empty Between range	`f.between(a, b)` where `a >= b`	`FALSE`

NOT Expression Simplifications¶

Rule	Before	After
NOT of TRUE	`NOT(TRUE)`	`FALSE`
NOT of FALSE	`NOT(FALSE)`	`TRUE`
Double negation	`NOT(NOT(x))`	`x`
NOT of equality	`NOT(f == v)`	`f != v`
NOT of inequality	`NOT(f != v)`	`f == v`
NOT of less-than	`NOT(f < v)`	`f >= v`
NOT of less-or-equal	`NOT(f <= v)`	`f > v`
NOT of greater-than	`NOT(f > v)`	`f <= v`
NOT of greater-or-equal	`NOT(f >= v)`	`f < v`
NOT of null check	`NOT(f.is_null())`	`f.is_not_null()`
NOT of not-null check	`NOT(f.is_not_null())`	`f.is_null()`
De Morgan's law (AND)	`NOT(a AND b)`	`NOT(a) OR NOT(b)`
De Morgan's law (OR)	`NOT(a OR b)`	`NOT(a) AND NOT(b)`

AND Expression Simplifications¶

Rule	Before	After
Empty AND	`AND()`	`TRUE`
Single operand	`AND(x)`	`x`
FALSE propagation	`AND(..., FALSE, ...)`	`FALSE`
TRUE elimination	`AND(..., TRUE, ...)`	`AND(...)`
Eq/Eq same value	`(f == v) AND (f == v)`	`f == v`
Eq/Eq different values	`(f == v1) AND (f == v2)`	`FALSE`
Eq/In intersection (member)	`(f == v) AND (f IN (v, ...))`	`f == v`
Eq/In intersection (non-member)	`(f == v) AND (f IN (...))`	`FALSE`
In/In intersection (empty)	`(f IN (v1, v2)) AND (f IN (v3, v4))`	`FALSE`
In/In intersection (single)	`(f IN (v1, v2)) AND (f IN (v2, v3))`	`f == v2`
In/In intersection (multiple)	`(f IN (v1, v2, v3)) AND (f IN (v2, v3, v4))`	`f IN (v2, v3)`

OR Expression Simplifications¶

Rule	Before	After
Empty OR	`OR()`	`FALSE`
Single operand	`OR(x)`	`x`
TRUE propagation	`OR(..., TRUE, ...)`	`TRUE`
FALSE elimination	`OR(..., FALSE, ...)`	`OR(...)`
Eq/Eq union	`(f == v1) OR (f == v2)`	`f IN (v1, v2)`
Eq/In union	`(f == v) OR (f IN (v2, v3))`	`f IN (v, v2, v3)`
In/In union	`(f IN (v1, v2)) OR (f IN (v3, v4))`	`f IN (v1, v2, v3, v4)`

Contradiction Detection (AND)¶

Pattern	Result
`(f == v) AND (f != v)`	`FALSE`
`f.is_null() AND f.is_not_null()`	`FALSE`
`(f < a) AND (f > b)` where `b >= a`	`FALSE`
`(f <= a) AND (f > a)`	`FALSE`
`(f >= b) AND (f < b)`	`FALSE`
`f.between(a, b) AND f.between(c, d)` — non-overlapping	`FALSE`
`f.between(a, b) AND f.between(c, d)` — overlapping	`f.between(max(a,c), min(b,d))`
`f.between(a, b) AND (f > c)` where `c >= b`	`FALSE`
`f.between(a, b) AND (f < c)` where `c <= a`	`FALSE`

Between Range Union (OR)¶

Pattern	Result
Overlapping ranges	`f.between(min(a,c), max(b,d))`
Adjacent ranges	`f.between(a, d)`

Tautology Detection (OR)¶

Pattern	Result
`(f == v) OR (f != v)`	`TRUE`
`f.is_null() OR f.is_not_null()`	`TRUE`
`(f < v) OR (f >= v)`	`TRUE`
`(f <= v) OR (f > v)`	`TRUE`

Optimization Tracking¶

result, records = optimize(expr)
for record in records:
    print(f"Applied: {record.reason}")
    print(f"Before:  {record.before}")
    print(f"After:   {record.after}")

Accumulate records across multiple calls:

my_records = []
result1, _ = optimize(expr1, my_records)
result2, _ = optimize(expr2, my_records)
# my_records contains steps from both calls

See Advanced Optimization Example for a complex real-world scenario.