diff options
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 5 | ||||
| -rw-r--r-- | plugins/nsatz/nsatz.ml | 51 |
2 files changed, 54 insertions, 2 deletions
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 3068b53470..b11d15e5ca 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont := match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; + let lci := fresh "lci" in set (lci:=lci0); + let lq := fresh "lq" in set (lq:=lq0); kont c rr lq lci end. @@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar := end in SplitPolyList ltac:(fun p lp => + let p21 := fresh "p21" in + let lp21 := fresh "lp21" in set (p21:=p) ; set (lp21:=lp); (* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + let q := fresh "q" in set (q := PEmul c (PEpow p21 r)); let Hg := fresh "Hg" in assert (Hg:check lp21 q (lci,lq) = true); diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 93dad18d98..36bce780bd 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -468,6 +468,44 @@ let theoremedeszeros lpol p = open Ideal +(* 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 + that has the same size than lp and where true indicates an + element that has been removed + *) +let rec clean_pol lp = + 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 + Warning: + the expansion is relative to the end of the list in reversed order + lp cannot have less elements than lb +*) +let expand_pol lb lp = + let rec aux lb lp = + match lb with + | [] -> lp + | true :: lb1 -> zeroP :: aux lb1 lp + | false :: lb1 -> + match lp with + [] -> assert false + | p :: lp1 -> p :: aux lb1 lp1 + in List.rev (aux lb (List.rev lp)) + let theoremedeszeros_termes lp = nvars:=0;(* mise a jour par term_pol_sparse *) List.iter set_nvars_term lp; @@ -518,20 +556,29 @@ let theoremedeszeros_termes lp = | [] -> assert false | p::lp1 -> let lpol = List.rev lp1 in + (* preprocessing : + we remove zero polynomials and duplicate that are not handled by in_ideal + lb is kept in order to fix the certificate in the post-processing + *) + let lpol, lb = clean_pol lpol in let (cert,lp0,p,_lct) = theoremedeszeros lpol p in info "cert ok\n"; let lc = cert.last_comb::List.rev cert.gb_comb in match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> + (* post-processing : we apply the correction for the last line *) + let lq = expand_pol lb lq in (* lci commence par les nouveaux polynomes *) - let m= !nvars in + let m = !nvars in let c = pol_sparse_to_term m (polconst m cert.coef) in let r = Pow(Zero,cert.power) in let lci = List.rev lci in + (* post-processing we apply the correction for the other lines *) + let lci = List.map (expand_pol lb) lci in let lci = List.map (List.map (pol_sparse_to_term m)) lci in let lq = List.map (pol_sparse_to_term m) lq in - info ("number of parametres: "^string_of_int nparam^"\n"); + info ("number of parameters: "^string_of_int nparam^"\n"); info "term computed\n"; (c,r,lci,lq) ) |