From 8438b97aa5c8d8464ec7389f7992520e2c176ae6 Mon Sep 17 00:00:00 2001
From: thery <thery@sophia.inria.fr>
Date: Wed, 6 Jul 2016 13:37:34 +0200
Subject: improved complexity in nsatz

we use a hashtable to reduce the complexity of creating
a duplicate-free list.
---
 plugins/nsatz/nsatz.ml4 | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 1230e64b9..592fbce67 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -472,12 +472,6 @@ let theoremedeszeros lpol p =
 
 open Ideal
 
-(* Check if the polynomial p is in the list lp *)
-let rec in_pol p lp =
-  match lp with
-  | [] -> false
-  | p1 :: lp1 -> if equal p p1 then true else in_pol p lp1
-
 (* Remove zero polynomials and duplicates from the list of polynomials lp
    Return (clp, lb)
    where clp is the reduced list and lb is a list of booleans
@@ -485,12 +479,19 @@ let rec in_pol p lp =
    element that has been removed
  *)
 let rec clean_pol lp =
-  match lp with
-  | [] -> [], []
-  | p :: lp1 -> 
-      let clp, lb = clean_pol lp1 in
-      if equal p zeroP || in_pol p clp then clp, true::lb 
-       else p :: clp, false::lb
+  let t = Hashpol.create 12 in
+  let find p = try Hashpol.find t p 
+               with 
+                 Not_found -> Hashpol.add t p true; false in
+  let rec aux lp =
+    match lp with
+    | [] -> [], []
+    | p :: lp1 -> 
+      let clp, lb = aux lp1 in
+      if equal p zeroP ||  find p then clp, true::lb 
+       else
+        (p :: clp, false::lb) in
+     aux lp
 
 (* Expand the list of polynomials lp putting zeros where the list of 
    booleans lb indicates there is a missing element 
-- 
cgit v1.2.3