aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL.md16
-rw-r--r--src/lia/lia.ml74
-rw-r--r--src/trace/smtCertif.ml4
-rw-r--r--src/trace/smtTrace.ml4
-rw-r--r--src/versions/native/structures.ml7
-rw-r--r--src/versions/standard/structures.ml7
6 files changed, 63 insertions, 49 deletions
diff --git a/INSTALL.md b/INSTALL.md
index 2fd328b..dd8ad2c 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -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
generated by cgit (git 2.34.1) at 2024-06-29 03:49:20 +0000