Predicates

Predicates let you embed comparisons, set membership, and typed constraints directly in a boolean expression.

Overview

A predicate is an atomic comparison involving a typed variable: age >= 18, region in {CA, US}, or tier == "gold". Logic Studio treats each unique predicate as a boolean atom — it's either true or false for any given input value.

Predicates are useful for modelling real-world gate logic where the inputs are not simple booleans but scalars, enumerations, or set memberships.

Feature-flag expression with predicates — the left panel shows Predicate Variables for age and region, each with type badges and predicate chips. — The feature-flag example. The Predicate Variables section shows `age` (with predicate `age >= 18`) and `region` (with predicate `region in {CA, US, UK}`).

Predicate syntax

Write predicates inline in the expression, wrapping in parentheses:

can_buy = (age >= 18) & (tier in {gold, platinum}) & !banned;

Each predicate becomes an atom in the boolean expression. The atom's truth value depends on the actual value of the typed variable at runtime.

Supported operators

Operator	Applies to	Example
`==`	number, string, enum	`status == "active"`
`!=`	number, string, enum	`country != "banned"`
`<`	number	`age < 18`
`<=`	number	`score <= 100`
`>`	number	`balance > 0`
`>=`	number	`age >= 18`
`in`	enum, string	`region in {CA, US, UK}`
`not-in`	enum, string	`country not-in {IR, KP}`

Limitation

Cross-variable arithmetic (e.g. a + b > c) is not supported. Each predicate must involve exactly one variable on the left side and a literal on the right. Z3 SMT can handle multi-variable constraints but the predicate UI does not model them.

Variable types

The Predicate Variables section in the left panel shows each predicate variable with a type badge. Types are detected automatically from the predicates used:

number — if any numeric comparison (<, >=, etc.) is used
enum — if an in/not-in with an explicit value list is used
string — if ==/!= with a string literal is used
UNTYPED — if no type can be determined (e.g. just a bare identifier used as a predicate)

Click the + button next to a variable to open the type editor and set the type, value range, or enum values explicitly. This enables richer bucket generation for the truth table and coverage panels.

Buckets

For a typed variable, Logic Studio generates buckets — mutually exclusive, collectively exhaustive value ranges that make each predicate constant. Each bucket becomes a row (or column group) in the truth table.

For a numeric variable with predicates age < 18 and age >= 21, the buckets are:

age < 18 — age < 18 is true, age >= 21 is false
age = 18 — both false
18 < age < 21 — both false
age = 21 — age >= 21 is true
age > 21 — age >= 21 is true

Enum variables enumerate each value in the declared value list plus an "other" bucket.

Contradictions & subsumption

Logic Studio's predicate theory module detects when two predicates over the same variable are logically contradictory or when one subsumes the other:

Contradiction: age < 18 AND age >= 18 — always false; the expression is unsatisfiable for that combination.
Subsumption: age < 18 AND age < 21 — the first implies the second; the conjunction equals the stricter predicate.

The solver and simplify panels will show these detections in their results.

Limitations

Predicate reasoning is per-variable only. Cross-variable constraints require Z3 SMT.
Set operations (union, intersection of sets) are not supported as expressions — only in/not-in with a literal set.
The truth table treats each predicate as an independent atom (a column). The actual relationship between predicates over the same variable is only modelled at the bucket level, not during standard truth table enumeration.
The simplifier (QM) operates on predicate atoms as opaque booleans. It doesn't know that age < 18 and age >= 18 are complements — that would require the SMT backend.