diff options
Diffstat (limited to 'src/lia/lia.ml')
| -rw-r--r-- | src/lia/lia.ml | 208 |
1 files changed, 208 insertions, 0 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml new file mode 100644 index 0000000..97415b9 --- /dev/null +++ b/src/lia/lia.ml @@ -0,0 +1,208 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +(*** Linking SMT Terms to Micromega Terms ***) +open Term +open Coqlib +open Declare +open Decl_kinds +open Entries +open Util +open Micromega +open Coq_micromega +open Errors + +open SmtMisc +open SmtForm +open SmtAtom + +(* morphism for expression over Z *) + +let rec pos_of_int i = + if i <= 1 + then XH + else + if i land 1 = 0 + 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 Z0 + else + if i > 0 + then Zpos (pos_of_int i) + else Zneg (pos_of_int (-i)) + +type my_tbl = + {tbl:(hatom,int) Hashtbl.t; mutable count:int} + +let get_atom_var tbl ha = + try Hashtbl.find tbl.tbl ha + with Not_found -> + let v = tbl.count in + Hashtbl.add tbl.tbl ha v; + tbl.count <- v + 1; + v + +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.XO (smt_Atom_to_micromega_pos ha) + | Auop(UO_xI, ha) -> + Micromega.XI (smt_Atom_to_micromega_pos ha) + | Acop CO_xH -> Micromega.XH + | _ -> raise Not_found + +let smt_Atom_to_micromega_Z ha = + match Atom.atom ha with + | Auop(UO_Zpos, ha) -> + Micromega.Zpos (smt_Atom_to_micromega_pos ha) + | Auop(UO_Zneg, ha) -> + Micromega.Zneg (smt_Atom_to_micromega_pos ha) + | Acop CO_Z0 -> Micromega.Z0 + | _ -> raise Not_found + +let rec smt_Atom_to_micromega_pExpr tbl ha = + match Atom.atom ha with + | 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 + 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 + 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 + PEsub(a, b) + | Auop (UO_Zopp, ha) -> + let a = smt_Atom_to_micromega_pExpr tbl ha in + PEopp a + | _ -> + try PEc (smt_Atom_to_micromega_Z ha) + with Not_found -> + let v = get_atom_var tbl ha in + PEX (pos_of_int v) + + +(* morphism for LIA proposition (=, >, ...) *) + +let smt_binop_to_micromega_formula tbl op ha hb = + let op = + match op with + | BO_Zlt -> OpLt + | BO_Zle -> OpLe + | BO_Zge -> OpGe + | BO_Zgt -> OpGt + | BO_eq _ -> OpEq + | _ -> 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 + {flhs = lhs; fop = op; frhs = rhs } + +let rec smt_Atom_to_micromega_formula tbl ha = + match Atom.atom ha with + | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb + | _ -> error + "lia.ml: smt_Atom_to_micromega_formula was expecting an LIA formula" + +(* specialized fold *) + +let default_constr = mkInt 0 +let default_tag = Mutils.Tag.from 0 +(* morphism for general formulas *) + +let binop_array g tbl op def t = + let n = Array.length t in + if n = 0 then + def + else + let aux = ref (g tbl t.(0)) in + for i = 1 to (n-1) do + aux := op !aux (g tbl t.(i)) + done; + !aux + +let rec smt_Form_to_coq_micromega_formula tbl l = + let v = + match Form.pform l with + | Fatom ha -> + A (smt_Atom_to_micromega_formula tbl ha, + default_tag,default_constr) + | 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 -> I (x,None,y)) TT l + | Fapp (Fiff, l) -> failwith "todo:Fiff" + | Fapp (Fite, l) -> failwith "todo:Fite" + | Fapp (Fnot2 _, l) -> + if Array.length l <> 1 then + failwith "Lia.smt_Form_to_coq_micromega_formula: wrong number of arguments for Fnot2" + else + smt_Form_to_coq_micromega_formula tbl l.(0) + in + if Form.is_pos l then v + else N(v) + +let binop_list tbl op def l = + match l with + | [] -> def + | f::l -> List.fold_left (fun x y -> op x (smt_Form_to_coq_micromega_formula tbl y)) (smt_Form_to_coq_micromega_formula tbl f) l + + +(* let rec binop_list tbl op def l = *) +(* match l with *) +(* | [] -> def *) +(* | [f] -> smt_Form_to_coq_micromega_formula tbl f *) +(* | f::l -> *) +(* op (smt_Form_to_coq_micromega_formula tbl f) (binop_list tbl op def l) *) + +(* and smt_Form_to_coq_micromega_formula tbl l = *) +(* let v = *) +(* match Form.pform l with *) +(* | Fatom ha -> *) +(* A (smt_Atom_to_micromega_formula tbl ha, *) +(* default_tag,default_constr) *) +(* | Fapp (Ftrue, _) -> TT *) +(* | Fapp (Ffalse, _) -> FF *) +(* | Fapp (Fand, l) -> binop_list tbl (fun x y -> C (x,y)) TT l *) +(* | Fapp (For, l) -> binop_list tbl (fun x y -> D (x,y)) FF l *) +(* | Fapp (Fxor, l) -> failwith "todo:Fxor" *) +(* | Fapp (Fimp, l) -> binop_list 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) -> smt_Form_to_coq_micromega_formula tbl l *) +(* in *) +(* if Form.is_pos l then v *) +(* else N(v) *) + + +let smt_clause_to_coq_micromega_formula tbl 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 = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in + tbl, f, tauto_lia f + |