Features and limits

Write a rule, inspect its inputs and output, simplify it, or compare it with another rule. The sections below explain the available analyses and when their limits matter.

Expression language

Feature	Use and limits
Boolean expressions	Use case-sensitive names, `true`/`false` or `1`/`0`, and NOT, AND, OR, XOR, implication (`->`) and equivalence (`<->`). Use parentheses to group terms.
Named bindings	Write `F = A & B;` and refer to `F` in later bindings. End each binding with a semicolon. Forward and cyclic references are not supported.
Don't-cares	Use the `?` suffix when either output is acceptable for Simplify. The dc Inputs control affects only the constrained Result summary.
Comments	Use `#` or `//` for a line comment and `/* ... */` for a block comment. Block comments do not nest.
Predicates	Compare one variable with a literal, such as `age >= 18`, or a literal set, such as `region in {CA, US}`. String comparisons support equality and set membership, not numeric ordering.

Analysis panels

Feature	Use and limits
Graph	View the active binding or choose Show all for connected bindings. Pan, zoom, and inspect how the expression is connected.
Truth Table	Inspect every combination of Boolean inputs and predicate columns. The row count doubles with each column; keep expressions small. Predicate columns can include combinations that are impossible for the underlying values.
Decision Table	View compact rules for the expression. Predicate columns describe conditions; use Predicate Variables to inspect value buckets.
Simplify	Minimise a Boolean expression as a two-level sum of products, for up to 12 atoms. Predicate reasoning uses Z3 when loaded; it may retain equivalent terms rather than find a fully minimal form. Expand Why? to follow the reasoning.
Rewrite	Convert to AND-of-ORs, OR-of-ANDs, or negation normal form; apply De Morgan, eliminate implications, factor terms, or read pseudocode.
K-map	Explore a Gray-coded grid for 2–6 variables. Outside that range, use Truth Table or Simplify.
Coverage	Generate branch, MC/DC, pairwise, prime-implicant, or full truth-table test vectors. Read the generated vectors and coverage summary for the selected criterion.
Equiv Diff	Compare two expressions. Row-by-row comparison is available for up to 14 pure Boolean variables. Larger comparisons return a verdict. Boolean differences include a distinguishing input; integer values from SMT counterexamples are not displayed.
Notebook	Save and load expressions on this browser. Export entries you want to retain before clearing browser data.

Predicate types and limits

Feature	Use and limits
Types and ranges	Click + beside a predicate variable to set its type, numeric range, or enum values. These declarations describe value buckets. Put required integer bounds in the expression itself.
Numeric and set reasoning	SMT/Z3 reasons about integer comparisons and sets of integer literals. String and enum predicates remain independent Boolean inputs, even with Z3 loaded. Use integer literals for SMT; decimal comparisons do not provide real-number reasoning. QM and Boolean-only SAT treat all predicates as independent inputs.
Unsupported syntax	Cross-variable arithmetic such as `a + b > c`, set union and intersection, optimisation objectives, and quantified formulas (`∀`, `∃`) are not supported. Use the existing satisfiability and tautology checks for Boolean questions.

Solver

Feature	Use and limits
Automatic selection	QM handles small Boolean simplifications. Equiv Diff selects SAT for more than 14 pure Boolean variables and SMT for predicates. The header controls simplification separately.
Z3 download	Z3 loads when requested or needed for SMT. Its WebAssembly file is about 33.7 MB decoded and about 7.6 MB over a gzip-compressed connection. It requires a browser with cross-origin isolation and shared-memory support.
Solving before Z3 is ready	Until Z3 is available, Boolean-only solving can treat predicates as independent inputs. Wait for Solver: SMT ✓ before relying on integer comparisons or numeric-set relationships.

Export and import

Feature	Use and limits
Code	Export JavaScript, Python, C, SQL, GitHub Actions conditions, and Lisp expressions. Coverage vectors can also be copied as code.
Graph images	Download PNG at screen resolution or SVG with the current theme colours.
Import	Import supported Boolean expressions from JavaScript, Python, SQL, or GitHub Actions. Arbitrary programs and idiomatic language constructs may not parse; inspect the loaded expression before using it.

Saving and sharing

Feature	Use and limits
Share link	The link restores expression source, display names, and declared variable types, ranges, and enum values. See Sharing for the fields carried by the link.
Local storage	Saved expressions and preferences stay in this browser. Export anything you need to retain before clearing browser data.

Interaction and browser support

Feature	Use and limits
Phone and tablet	Use the editor, examples, result views, and share controls in the narrow layout. Pan and zoom the graph on touch; edit the expression in the text editor.
Keyboard	Open command search with `⌘K` or `Ctrl+K`. See keyboard shortcuts for panel navigation and applying results.
Language and theme	Choose Basic for plain-language labels or Advanced for specialised terms. Teaching mode reveals explanations from info buttons. Choose a light, dark, or system theme.
Nonvisual access	Use the text editor, Truth Table, Decision Table, and copied results to inspect the expression without the visual graph. Graph relationships require visual inspection.
Offline use	After an online visit, cached app files support offline editing and Boolean analysis. Z3 is a separate download and may be unavailable if it has not been cached. Connect before starting an SMT task.
Install app	Use the install control where the browser offers it. On Safari, use Add to Home Screen from the share menu.

Choose a task

Follow the how-to guide to simplify a rule, inspect inputs, compare expressions, or share your work.