diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2017-10-03 11:20:59 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2017-10-03 11:20:59 +0200 |
commit | 48e123caddd6a4c4edd60d8f39b78a5421418f40 (patch) | |
tree | 983e804bacb76874c1f10f8f5319b21517f751bc | |
parent | ca5213e2a653640cab6d98c1b0e799262b6be33d (diff) | |
download | smtcoq-48e123caddd6a4c4edd60d8f39b78a5421418f40.tar.gz smtcoq-48e123caddd6a4c4edd60d8f39b78a5421418f40.zip |
Compiles with both versions of Coq
-rw-r--r-- | INSTALL.md | 16 | ||||
-rw-r--r-- | src/lia/lia.ml | 74 | ||||
-rw-r--r-- | src/trace/smtCertif.ml | 4 | ||||
-rw-r--r-- | src/trace/smtTrace.ml | 4 | ||||
-rw-r--r-- | src/versions/native/structures.ml | 7 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 7 |
6 files changed, 63 insertions, 49 deletions
@@ -14,7 +14,7 @@ In either case, you will also need to install the provers you want to use (see below). -## Installation via opam +## Installation via opam (uses Coq-8.5) Simply add the coq-extra-dev repo to opam: ``` @@ -26,19 +26,19 @@ opam install coq-smtcoq ``` -## Installation from the sources +## Installation from the sources (uses Coq-8.6 or native-coq) -You can also build SMTCoq from the sources, using either Coq 8.5 or the +You can also build SMTCoq from the sources, using either Coq 8.6 or the [version of Coq with native data-structures](https://github.com/smtcoq/native-coq). -We recommend Coq 8.5 for standard use, and native-coq for uses that +We recommend Coq 8.6 for standard use, and native-coq for uses that require very efficient computation (such as checking big certificates). -### Installation with Coq 8.5 +### Installation with Coq 8.6 -1. Download the last stable version of Coq 8.5: +1. Download the last stable version of Coq 8.6: ``` -wget https://coq.inria.fr/distrib/V8.5pl2/files/coq-8.5pl2.tar.gz +wget https://coq.inria.fr/distrib/8.6.1/files/coq-8.6.1.tar.gz ``` and compile it by following the instructions available in the repository. We recommand that you do not install it, but only compile @@ -51,7 +51,7 @@ make 2. Set an environment variable COQBIN to the directory where Coq's binaries are; for instance: ``` -export COQBIN=/home/jdoe/coq-8.5pl2/bin/ +export COQBIN=/home/jdoe/coq-8.6.1/bin/ ``` (the final slash is mandatory). diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 07064bb..589d59a 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -21,8 +21,8 @@ open Declare open Decl_kinds open Entries open Util -(* open Micromega *) -(* open Coq_micromega *) +open Structures.Micromega_plugin_Micromega +open Structures.Micromega_plugin_Coq_micromega open SmtMisc open SmtForm @@ -32,19 +32,19 @@ open SmtAtom let rec pos_of_int i = if i <= 1 - then Micromega_plugin.Micromega.XH + then XH else if i land 1 = 0 - then Micromega_plugin.Micromega.XO(pos_of_int (i lsr 1)) - else Micromega_plugin.Micromega.XI(pos_of_int (i lsr 1)) + then XO(pos_of_int (i lsr 1)) + else XI(pos_of_int (i lsr 1)) let z_of_int i = if i = 0 - then Micromega_plugin.Micromega.Z0 + then Z0 else if i > 0 - then Micromega_plugin.Micromega.Zpos (pos_of_int i) - else Micromega_plugin.Micromega.Zneg (pos_of_int (-i)) + then Zpos (pos_of_int i) + else Zneg (pos_of_int (-i)) type my_tbl = {tbl:(hatom,int) Hashtbl.t; mutable count:int} @@ -62,19 +62,19 @@ let create_tbl n = {tbl=Hashtbl.create n;count=1} let rec smt_Atom_to_micromega_pos ha = match Atom.atom ha with | Auop(UO_xO, ha) -> - Micromega_plugin.Micromega.XO (smt_Atom_to_micromega_pos ha) + XO (smt_Atom_to_micromega_pos ha) | Auop(UO_xI, ha) -> - Micromega_plugin.Micromega.XI (smt_Atom_to_micromega_pos ha) - | Acop CO_xH -> Micromega_plugin.Micromega.XH + XI (smt_Atom_to_micromega_pos ha) + | Acop CO_xH -> XH | _ -> raise Not_found let smt_Atom_to_micromega_Z ha = match Atom.atom ha with | Auop(UO_Zpos, ha) -> - Micromega_plugin.Micromega.Zpos (smt_Atom_to_micromega_pos ha) + Zpos (smt_Atom_to_micromega_pos ha) | Auop(UO_Zneg, ha) -> - Micromega_plugin.Micromega.Zneg (smt_Atom_to_micromega_pos ha) - | Acop CO_Z0 -> Micromega_plugin.Micromega.Z0 + Zneg (smt_Atom_to_micromega_pos ha) + | Acop CO_Z0 -> Z0 | _ -> raise Not_found let rec smt_Atom_to_micromega_pExpr tbl ha = @@ -82,23 +82,23 @@ let rec smt_Atom_to_micromega_pExpr tbl ha = | Abop (BO_Zplus, ha, hb) -> let a = smt_Atom_to_micromega_pExpr tbl ha in let b = smt_Atom_to_micromega_pExpr tbl hb in - Micromega_plugin.Micromega.PEadd(a, b) + PEadd(a, b) | Abop (BO_Zmult, ha, hb) -> let a = smt_Atom_to_micromega_pExpr tbl ha in let b = smt_Atom_to_micromega_pExpr tbl hb in - Micromega_plugin.Micromega.PEmul(a, b) + PEmul(a, b) | Abop (BO_Zminus, ha, hb) -> let a = smt_Atom_to_micromega_pExpr tbl ha in let b = smt_Atom_to_micromega_pExpr tbl hb in - Micromega_plugin.Micromega.PEsub(a, b) + PEsub(a, b) | Auop (UO_Zopp, ha) -> let a = smt_Atom_to_micromega_pExpr tbl ha in - Micromega_plugin.Micromega.PEopp a + PEopp a | _ -> - try Micromega_plugin.Micromega.PEc (smt_Atom_to_micromega_Z ha) + try PEc (smt_Atom_to_micromega_Z ha) with Not_found -> let v = get_atom_var tbl ha in - Micromega_plugin.Micromega.PEX (pos_of_int v) + PEX (pos_of_int v) (* morphism for LIA proposition (=, >, ...) *) @@ -106,17 +106,17 @@ let rec smt_Atom_to_micromega_pExpr tbl ha = let smt_binop_to_micromega_formula tbl op ha hb = let op = match op with - | BO_Zlt -> Micromega_plugin.Micromega.OpLt - | BO_Zle -> Micromega_plugin.Micromega.OpLe - | BO_Zge -> Micromega_plugin.Micromega.OpGe - | BO_Zgt -> Micromega_plugin.Micromega.OpGt - | BO_eq _ -> Micromega_plugin.Micromega.OpEq + | BO_Zlt -> OpLt + | BO_Zle -> OpLe + | BO_Zge -> OpGe + | BO_Zgt -> OpGt + | BO_eq _ -> OpEq | _ -> Structures.error "lia.ml: smt_binop_to_micromega_formula expecting a formula" in let lhs = smt_Atom_to_micromega_pExpr tbl ha in let rhs = smt_Atom_to_micromega_pExpr tbl hb in - {Micromega_plugin.Micromega.flhs = lhs; Micromega_plugin.Micromega.fop = op; Micromega_plugin.Micromega.frhs = rhs } + {flhs = lhs; fop = op; frhs = rhs } let rec smt_Atom_to_micromega_formula tbl ha = match Atom.atom ha with @@ -127,7 +127,7 @@ let rec smt_Atom_to_micromega_formula tbl ha = (* specialized fold *) let default_constr = mkInt 0 -let default_tag = Micromega_plugin.Mutils.Tag.from 0 +let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0 (* morphism for general formulas *) let binop_array g tbl op def t = @@ -145,14 +145,14 @@ let rec smt_Form_to_coq_micromega_formula tbl l = let v = match Form.pform l with | Fatom ha -> - Micromega_plugin.Coq_micromega.A (smt_Atom_to_micromega_formula tbl ha, + A (smt_Atom_to_micromega_formula tbl ha, default_tag,default_constr) - | Fapp (Ftrue, _) -> Micromega_plugin.Coq_micromega.TT - | Fapp (Ffalse, _) -> Micromega_plugin.Coq_micromega.FF - | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.C (x,y)) Micromega_plugin.Coq_micromega.TT l - | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.D (x,y)) Micromega_plugin.Coq_micromega.FF l + | Fapp (Ftrue, _) -> TT + | Fapp (Ffalse, _) -> FF + | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l + | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> D (x,y)) FF l | Fapp (Fxor, l) -> failwith "todo:Fxor" - | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.I (x,None,y)) Micromega_plugin.Coq_micromega.TT l + | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> I (x,None,y)) TT l | Fapp (Fiff, l) -> failwith "todo:Fiff" | Fapp (Fite, l) -> failwith "todo:Fite" | Fapp (Fnot2 _, l) -> @@ -162,7 +162,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = smt_Form_to_coq_micromega_formula tbl l.(0) in if Form.is_pos l then v - else Micromega_plugin.Coq_micromega.N(v) + else N(v) let binop_list tbl op def l = match l with @@ -198,11 +198,11 @@ let binop_list tbl op def l = let smt_clause_to_coq_micromega_formula tbl cl = - binop_list tbl (fun x y -> Micromega_plugin.Coq_micromega.C(x,y)) Micromega_plugin.Coq_micromega.TT (List.map Form.neg cl) + binop_list tbl (fun x y -> C(x,y)) TT (List.map Form.neg cl) (* call to micromega solver *) let build_lia_certif cl = let tbl = create_tbl 13 in - let f = Micromega_plugin.Coq_micromega.I(smt_clause_to_coq_micromega_formula tbl cl, None, Micromega_plugin.Coq_micromega.FF) in - tbl, f, Micromega_plugin.Coq_micromega.tauto_lia f + let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in + tbl, f, tauto_lia f diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 868a311..e4ed262 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -99,11 +99,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Micromega_plugin.Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Micromega_plugin.Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index c372310..4815a77 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -324,12 +324,12 @@ let to_coq to_lit interp (cstep, mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|] | LiaMicromega (cl,d) -> let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in - let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm|]) in + let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in mklApp cLiaMicromega [|out_c c; cl'; c'|] | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|] | SplArith (orig,res,l) -> let res' = out_f res in - let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm|]) in + let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in mklApp cSplArith [|out_c c; out_c orig; res'; l'|] | SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|] | Hole (prem_id, concl) -> diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 9a56d43..589e772 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -123,3 +123,10 @@ let ppconstr_lsimpleconstr = Ppconstr.lsimple let constrextern_extern_constr = let env = Global.env () in Constrextern.extern_constr false env + + +(* Old packaging of plugins *) +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega +module Micromega_plugin_Micromega = Micromega +module Micromega_plugin_Mutils = Mutils diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 45a8ca4..57838ee 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -157,3 +157,10 @@ let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr let constrextern_extern_constr = let env = Global.env () in Constrextern.extern_constr false env (Evd.from_env env) + + +(* New packaging of plugins *) +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega +module Micromega_plugin_Micromega = Micromega_plugin.Micromega +module Micromega_plugin_Mutils = Micromega_plugin.Mutils |