diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 17:35:17 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-05-28 17:35:17 +0200 |
commit | a3a63ab0bceb12f03bac91ef7461061f1cb20af1 (patch) | |
tree | 478ca52f88e72d369d174e6edeba63dfe4827b1c /src | |
parent | 1f414ad1cfcef2e8cfb59659cf743401716bc90c (diff) | |
parent | 52980aab9541a12619eb9191a94e9b2ba4684447 (diff) | |
download | smtcoq-a3a63ab0bceb12f03bac91ef7461061f1cb20af1.tar.gz smtcoq-a3a63ab0bceb12f03bac91ef7461061f1cb20af1.zip |
Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11
Diffstat (limited to 'src')
-rw-r--r-- | src/lia/lia.ml | 199 | ||||
-rw-r--r-- | src/versions/native/structures.ml | 2 | ||||
-rw-r--r-- | src/versions/native/structures.mli | 2 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 5 | ||||
-rw-r--r-- | src/versions/standard/structures.mli | 3 |
5 files changed, 10 insertions, 201 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 1595ff7..53dbf6d 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -151,200 +151,19 @@ let binop_list tbl op def l = let smt_clause_to_coq_micromega_formula tbl cl = binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) - -(* backported from Coq *) -type ('option,'a,'prf,'model) prover = { - name : string ; (* name of the prover *) - get_option : unit ->'option ; (* find the options of the prover *) - prover : ('option * 'a list) -> ('prf, 'model) Structures.Micromega_plugin_Certificate.res ; (* the prover itself *) - hyps : 'prf -> Structures.Micromega_plugin_Mutils.ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) - compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) - pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) - pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) -} - -let lia_enum = ref true -let max_depth = max_int -let lia_proof_depth = ref max_depth -let get_lia_option () = - (!Structures.Micromega_plugin_Certificate.use_simplex,!lia_enum,!lia_proof_depth) - -let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Structures.Micromega_plugin_Micromega.denorm e , o) l) - -module CacheZ = Structures.Micromega_plugin_Persistent_cache.PHashtable(struct - type prover_option = bool * bool* int - type t = prover_option * ((Structures.Micromega_plugin_Micromega.z Structures.Micromega_plugin_Micromega.pol * Structures.Micromega_plugin_Micromega.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Structures.Micromega_plugin_Certificate.lia ce b) s) - -let xhyps_of_cone base acc prf = - let open Structures.Micromega_plugin_Micromega in - - let rec xtract e acc = - match e with - | PsatzC _ | PsatzZ | PsatzSquare _ -> acc - | PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in - if n >= base - then Structures.Micromega_plugin_Mutils.ISet.add (n-base) acc - else acc - | PsatzMulC(_,c) -> xtract c acc - | PsatzAdd(e1,e2) | PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in - - xtract prf acc - -let hyps_of_pt pt = - let open Structures.Micromega_plugin_Micromega in - - let rec xhyps base pt acc = - match pt with - | DoneProof -> acc - | RatProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c) - | CutProof (c, pt) -> xhyps (base + 1) pt (xhyps_of_cone base acc c) - | EnumProof (c1, c2, l) -> - let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in - List.fold_left (fun s x -> xhyps (base + 1) x s) s l - | ExProof (_, pt) -> xhyps (base + 3) pt acc - in - - xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty - -let compact_cone prf f = - let open Structures.Micromega_plugin_Micromega in - - let np n = Structures.Micromega_plugin_Mutils.CamlToCoq.nat (f (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)) in - - let rec xinterp prf = - match prf with - | PsatzC _ | PsatzZ | PsatzSquare _ -> prf - | PsatzIn n -> PsatzIn (np n) - | PsatzMulC(e,c) -> PsatzMulC(e,xinterp c) - | PsatzAdd(e1,e2) -> PsatzAdd(xinterp e1,xinterp e2) - | PsatzMulE(e1,e2) -> PsatzMulE(xinterp e1,xinterp e2) in - - xinterp prf - -let compact_pt pt f = - let open Structures.Micromega_plugin_Micromega in - let translate ofset x = if x < ofset then x else f (x - ofset) + ofset in - let rec compact_pt ofset pt = - match pt with - | DoneProof -> DoneProof - | RatProof (c, pt) -> - RatProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt) - | CutProof (c, pt) -> - CutProof (compact_cone c (translate ofset), compact_pt (ofset + 1) pt) - | EnumProof (c1, c2, l) -> - EnumProof - ( compact_cone c1 (translate ofset) - , compact_cone c2 (translate ofset) - , map (fun x -> compact_pt (ofset + 1) x) l ) - | ExProof (x, pt) -> ExProof (x, compact_pt (ofset + 3) pt) - in - compact_pt 0 pt - -let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) - -let pp_positive o x = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.positive x) - -let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x)) - -let pp_list op cl elt o l = - let rec _pp o l = - match l with - | [] -> () - | [e] -> Printf.fprintf o "%a" elt e - | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in - Printf.fprintf o "%s%a%s" op _pp l cl - -let pp_pol pp_c o e = - let open Structures.Micromega_plugin_Micromega in - let rec pp_pol o e = - match e with - | Pc n -> Printf.fprintf o "Pc %a" pp_c n - | Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol - | PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in - pp_pol o e - -let pp_psatz pp_z o e = - let open Structures.Micromega_plugin_Micromega in - let rec pp_cone o e = - match e with - | PsatzIn n -> - Printf.fprintf o "(In %a)%%nat" pp_nat n - | PsatzMulC(e,c) -> - Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c - | PsatzSquare e -> - Printf.fprintf o "(%a^2)" (pp_pol pp_z) e - | PsatzAdd(e1,e2) -> - Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 - | PsatzMulE(e1,e2) -> - Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 - | PsatzC p -> - Printf.fprintf o "(%a)%%positive" pp_z p - | PsatzZ -> - Printf.fprintf o "0" in - pp_cone o e - -let rec pp_proof_term o p = - let open Structures.Micromega_plugin_Micromega in - match p with - | DoneProof -> Printf.fprintf o "D" - | RatProof (cone, rst) -> - Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | CutProof (cone, rst) -> - Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | EnumProof (c1, c2, rst) -> - Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 - (pp_list "[" "]" pp_proof_term) - rst - | ExProof (p, prf) -> - Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf - -let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let find_witness p polys1 = - let open Structures.Micromega_plugin_Certificate in - let polys1 = List.map fst polys1 in - match p.prover (p.get_option (), polys1) with - | Model m -> Model m - | Unknown -> Unknown - | Prf prf -> Prf(prf,p) - -let witness_list prover l = - let open Structures.Micromega_plugin_Certificate in +let tauto_lia ff = + let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in let rec xwitness_list l = match l with - | [] -> Prf [] + | [] -> Some [] | e :: l -> match xwitness_list l with - | Model (m,e) -> Model (m,e) - | Unknown -> Unknown - | Prf l -> - match find_witness prover e with - | Model m -> Model (m,e) - | Unknown -> Unknown - | Prf w -> Prf (w::l) in - xwitness_list l - -let witness_list_tags = witness_list - -let tauto_lia ff = - let prover = linear_Z in - let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in - match witness_list_tags prover cnf_ff with - | Structures.Micromega_plugin_Certificate.Prf l -> Some (List.map fst l) - | _ -> None + | None -> None + | Some l -> + match Structures.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> Structures.Micromega_plugin_Micromega.denorm e, o) e) with + | Structures.Micromega_plugin_Certificate.Prf w -> Some (w::l) + | _ -> None in + xwitness_list cnf_ff (* call to micromega solver *) let build_lia_certif cl = diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 0738801..435a1a1 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -140,9 +140,7 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Mutils = Mutils module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega let micromega_coq_proofTerm = Coq_micromega.M.coq_proofTerm diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index d8071d9..f2775a6 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -82,9 +82,7 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Mutils = Mutils module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index a89d569..11dccbf 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -159,10 +159,7 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega -module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache let micromega_coq_proofTerm = (* Cannot contain evars *) @@ -170,7 +167,7 @@ let micromega_coq_proofTerm = let micromega_dump_proof_term p = (* Cannot contain evars *) - EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p) + EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) (* Tactics *) diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 52103bc..1a82d96 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -90,10 +90,7 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega -module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr |