Implement equivalence breaking for strong equivalence decomposition

potassco · Aug 20, 2024 · 2d36dc2 · 2d36dc2
1 parent 6590cbd
commit 2d36dc2
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/verifying/task/strong_equivalence.rs b/src/verifying/task/strong_equivalence.rs
@@ -78,7 +78,10 @@ impl Task for StrongEquivalenceTask {
             right = crate::simplifying::fol::classic::simplify(right);
         }
 
-        // TODO: Break equivalences, if requested
+        if self.break_equivalences {
+            left = crate::breaking::fol::ht::break_equivalences_theory(left);
+            right = crate::breaking::fol::ht::break_equivalences_theory(right);
+        }
 
         let mut problems = Vec::new();
         if matches!(