Home

Term Flattening

EUF pre-processing — transform a cube into an equisatisfiable flat cube, one rule at a time

EUF / Pre-processing
Cube Input (literals)
Syntax: = equality  |  != or ≠ disequality  |  ! or ¬ or ~ negation  |  f(x,y) function application  |  P(x) predicate  |  literals separated by ,
Examples:
Flattening Rules
What can I do?
Load a cube to begin.
Current Cube
Load a cube to begin.
Fresh Variables
No fresh variables introduced yet.
Step Explanation

Apply a flattening rule to see a step-by-step explanation.

Step History
Apply Flattening Rule
Choose a non-flat literal. The corresponding rule will be applied, introducing a fresh variable. 

  






  
Lab Files


  

    

      🐍 Source Code ▼
    

    

      
        flattern.py
        PY
        View
      
      
        flattern-debug.py
        PY
        View
      
    

  


  

    

      📁 Benchmarks ▼