Theory Combo Viz

Welcome to the theory combination visualizer!

Reference paper

Usage

Write your formula in the theory of ints and sets, and then you can check the steps done to verify satisfiability!

Syntax
  • Equality: ==, !=
  • Sets: You can use brackets like so - {1, 2, ...},
  • Variables: Alphanumeric word
  • Constants: integers
  • Arithmetic: +, -, * /
  • Int comparison: >, <, >=, <=

When writing variables, it is good practice to explicitly define its type. However, variables types can still be inferred for convenience.

Limitations
  • Limited theories
  • No nested data structures
  • Very little fancy animations 😢
  • Not mobile responsive (due to laziness)

Formula variables

Variables type can be inferred or explicit

    Examples

    • a == 2 + 3 ∧ b == 5 * x ∧ x == 1 ∧ (a ∉ S ∨ b ∈ S)
    • S == {2 + 3} ∧ T == {1 + 4} ∧ S \ T == ∅
    • S == {2 + 3} ∧ T == {1 + 4} ∧ S != T
    • x == (5 * 4 / 10) + 1 ∧ s == ({1 + 2} ∪ {x}) \ {3} ∧ s != ∅
    • x != y ∧ x ∩ y == ∅ ∧ 1 ∈ x
    • x != ∅ ∧ y != ∅ ∧ x ∪ y == ∅ ∧ 1 ∉ x
    • x == {3 + 5, 1} ∧ 8 ∈ x ∧ 2 - 1 ∉ x