Home

Congruence Closure

EUF theory solver — decide satisfiability of a flat cube using equivalence classes

EUF / CC Algorithm
Flat Cube Input
⚠ Formula is not flat — CC requires a flat cube
The Congruence Closure algorithm requires all literals to be in flat form.
You can auto-flatten here, or open the Flatten Lab to do it step by step.
Input a flat cube: equalities =, disequalities !=, predicates P(x,y). All arguments must be variables. Literals separated by ,.
Examples:
CC Actions
Auto-Solve
Applies top-level, then congruence, then fail check, stops at SAT/UNSAT.
What can I do?
Load a flat cube to begin.
Flat Cube
Load a formula to see literals here.
Equivalence Classes M
Initialize to see equivalence classes.
Step History
No steps yet.
Top-Level Rule
An equality in the cube whose two sides are in different classes. Choose one to merge.
Congruence Rule
Two function applications with congruent arguments but in different classes. Choose one to merge. 

  






  
Lab Files


  

    

      🐍 Source Code ▼
    

    

      
        cc-solver.py
        PY
        View
      
      
        cc-solver-debug.py
        PY
        View
      
    

  


  

    

      📁 Benchmarks ▼