diff options
Diffstat (limited to 'src/lia/lia.ml')
-rw-r--r-- | src/lia/lia.ml | 74 |
1 files changed, 37 insertions, 37 deletions
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 |