From 8aa451b1e31889ef2beffbbd4764190ca61939a6 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Wed, 2 Sep 2020 15:44:51 +0200
Subject: [micromega] Optimised cnf in case an hypothesis is trivially False.

This optimisation reduces (sometimes) the dependencies of a proof.
---
 plugins/micromega/micromega.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index b231779c7b..1556ec31b5 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1384,11 +1384,13 @@ let rxcnf_or unsat deduce rXCNF polarity k e1 e2 =
 let rxcnf_impl unsat deduce rXCNF polarity k e1 e2 =
   let e3,t1 = rXCNF (negb polarity) k e1 in
   if polarity
-  then if is_cnf_ff e3
-       then rXCNF polarity k e2
-       else let e4,t2 = rXCNF polarity k e2 in
-            let f',t' = ror_cnf_opt unsat deduce e3 e4 in
-            f',(rev_append t1 (rev_append t2 t'))
+  then if is_cnf_tt e3
+       then e3,t1
+       else if is_cnf_ff e3
+            then rXCNF polarity k e2
+            else let e4,t2 = rXCNF polarity k e2 in
+                 let f',t' = ror_cnf_opt unsat deduce e3 e4 in
+                 f',(rev_append t1 (rev_append t2 t'))
   else let e4,t2 = rXCNF polarity k e2 in
        (and_cnf_opt e3 e4),(rev_append t1 t2)
 
-- 
cgit v1.2.3