summaryrefslogtreecommitdiff
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r--plugins/micromega/coq_micromega.ml887
1 files changed, 645 insertions, 242 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index cce0a728..e4b58a56 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -18,6 +18,7 @@
open Pp
open Mutils
+open Goptions
(**
* Debug flag
@@ -37,6 +38,53 @@ let time str f x =
flush stdout);
res
+
+(* Limit the proof search *)
+
+let max_depth = max_int
+
+(* Search limit for provers over Q R *)
+let lra_proof_depth = ref max_depth
+
+
+(* Search limit for provers over Z *)
+let lia_enum = ref true
+let lia_proof_depth = ref max_depth
+
+let get_lia_option () =
+ (!lia_enum,!lia_proof_depth)
+
+let get_lra_option () =
+ !lra_proof_depth
+
+
+
+let _ =
+
+ let int_opt l vref =
+ {
+ optsync = true;
+ optdepr = false;
+ optname = List.fold_right (^) l "";
+ optkey = l ;
+ optread = (fun () -> Some !vref);
+ optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v))
+ } in
+
+ let lia_enum_opt =
+ {
+ optsync = true;
+ optdepr = false;
+ optname = "Lia Enum";
+ optkey = ["Lia";"Enum"];
+ optread = (fun () -> !lia_enum);
+ optwrite = (fun x -> lia_enum := x)
+ } in
+ let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
+ let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
+ let _ = declare_bool_option lia_enum_opt in
+ ()
+
(**
* Initialize a tag type to the Tag module declaration (see Mutils).
*)
@@ -99,6 +147,17 @@ let rec map_atoms fct f =
| N f -> N(map_atoms fct f)
| I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2)
+let rec map_prop fct f =
+ match f with
+ | TT -> TT
+ | FF -> FF
+ | X x -> X (fct x)
+ | A (at,tg,cstr) -> A(at,tg,cstr)
+ | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2)
+ | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2)
+ | N f -> N(map_prop fct f)
+ | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2)
+
(**
* Collect the identifiers of a (string of) implications. Implication labels
* are inherited from Coq/CoC's higher order dependent type constructor (Pi).
@@ -244,7 +303,8 @@ let rec add_term t0 = function
*)
module ISet = Set.Make(Int)
-
+module IMap = Map.Make(Int)
+
(**
* Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
* elements of m that are at position i0,...,iN.
@@ -303,7 +363,8 @@ struct
let r_modules =
[["Coq";"Reals" ; "Rdefinitions"];
["Coq";"Reals" ; "Rpow_def"] ;
-]
+ ["Coq";"Reals" ; "Raxioms"] ;
+ ]
let z_modules = [["Coq";"ZArith";"BinInt"]]
@@ -322,6 +383,8 @@ struct
let coq_and = lazy (init_constant "and")
let coq_or = lazy (init_constant "or")
let coq_not = lazy (init_constant "not")
+ let coq_not_gl_ref = (Nametab.locate ( Libnames.qualid_of_string "Coq.Init.Logic.not"))
+
let coq_iff = lazy (init_constant "iff")
let coq_True = lazy (init_constant "True")
let coq_False = lazy (init_constant "False")
@@ -359,6 +422,7 @@ struct
let coq_Qmake = lazy (constant "Qmake")
let coq_Rcst = lazy (constant "Rcst")
+
let coq_C0 = lazy (m_constant "C0")
let coq_C1 = lazy (m_constant "C1")
let coq_CQ = lazy (m_constant "CQ")
@@ -415,8 +479,9 @@ struct
let coq_Rdiv = lazy (r_constant "Rdiv")
let coq_Rinv = lazy (r_constant "Rinv")
let coq_Rpower = lazy (r_constant "pow")
+ let coq_IZR = lazy (r_constant "IZR")
let coq_IQR = lazy (constant "IQR")
- let coq_IZR = lazy (constant "IZR")
+
let coq_PEX = lazy (constant "PEX" )
let coq_PEc = lazy (constant"PEc")
@@ -896,8 +961,20 @@ struct
let (env,n) = _add l ( n+1) v in
(e::env,n) in
let (env, n) = _add env 1 v in
- (env, CamlToCoq.idx n)
+ (env, CamlToCoq.positive n)
+
+ let get_rank env v =
+ let rec _get_rank env n =
+ match env with
+ | [] -> raise (Invalid_argument "get_rank")
+ | e::l ->
+ if eq_constr e v
+ then n
+ else _get_rank l (n+1) in
+ _get_rank env 1
+
+
let empty = []
let elements env = env
@@ -910,7 +987,7 @@ struct
let parse_expr parse_constant parse_exp ops_spec env term =
if debug
- then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
+ then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
(*
let constant_or_variable env term =
@@ -947,7 +1024,7 @@ struct
let (expr,env) = parse_expr env args.(0) in
let power = (parse_exp expr args.(1)) in
(power , env)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(* if the exponent is a variable *)
let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
end
@@ -994,7 +1071,7 @@ struct
coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ;
coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ;
coq_Rmult , (fun x y -> Mc.CMult(x,y)) ;
- coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;
+ (* coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*)
]
let rec rconstant term =
@@ -1016,10 +1093,14 @@ struct
with
ParseError ->
match op with
- | op when Constr.equal op (Lazy.force coq_Rinv) -> Mc.CInv(rconstant args.(0))
- | op when Constr.equal op (Lazy.force coq_IQR) -> Mc.CQ (parse_q args.(0))
-(* | op when op = Lazy.force coq_IZR -> Mc.CZ (parse_z args.(0))*)
- | _ -> raise ParseError
+ | op when Constr.equal op (Lazy.force coq_Rinv) ->
+ let arg = rconstant args.(0) in
+ if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH}
+ then raise ParseError (* This is a division by zero -- no semantics *)
+ else Mc.CInv(arg)
+ | op when Constr.equal op (Lazy.force coq_IQR) -> Mc.CQ (parse_q args.(0))
+ | op when Constr.equal op (Lazy.force coq_IZR) -> Mc.CZ (parse_z args.(0))
+ | _ -> raise ParseError
end
| _ -> raise ParseError
@@ -1027,7 +1108,7 @@ struct
let rconstant term =
if debug
- then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
let res = rconstant term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1067,7 +1148,7 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
if debug
- then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
match kind_of_term cstr with
| App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
@@ -1094,10 +1175,6 @@ struct
| N (a) -> Mc.N(f2f a)
| I(a,_,b) -> Mc.I(f2f a,f2f b)
- let is_prop t =
- match t with
- | Names.Anonymous -> true (* Not quite right *)
- | Names.Name x -> false
let mkC f1 f2 = C(f1,f2)
let mkD f1 f2 = D(f1,f2)
@@ -1119,34 +1196,40 @@ struct
try
let (at,env) = parse_atom env t gl in
(A(at,tg,t), env,Tag.next tg)
- with e when Errors.noncritical e -> (X(t),env,tg) in
+ with e when CErrors.noncritical e -> (X(t),env,tg) in
+ let is_prop term =
+ let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
+ Term.is_prop_sort sort in
+
let rec xparse_formula env tg term =
- match kind_of_term term with
+ match kind_of_term term with
| App(l,rst) ->
- (match rst with
- | [|a;b|] when eq_constr l (Lazy.force coq_and) ->
- let f,env,tg = xparse_formula env tg a in
- let g,env, tg = xparse_formula env tg b in
- mkformula_binary mkC term f g,env,tg
- | [|a;b|] when eq_constr l (Lazy.force coq_or) ->
- let f,env,tg = xparse_formula env tg a in
- let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkD term f g,env,tg
- | [|a|] when eq_constr l (Lazy.force coq_not) ->
- let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
- | [|a;b|] when eq_constr l (Lazy.force coq_iff) ->
- let f,env,tg = xparse_formula env tg a in
- let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkIff term f g,env,tg
- | _ -> parse_atom env tg term)
- | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) ->
+ (match rst with
+ | [|a;b|] when eq_constr l (Lazy.force coq_and) ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env, tg = xparse_formula env tg b in
+ mkformula_binary mkC term f g,env,tg
+ | [|a;b|] when eq_constr l (Lazy.force coq_or) ->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env,tg = xparse_formula env tg b in
+ mkformula_binary mkD term f g,env,tg
+ | [|a|] when eq_constr l (Lazy.force coq_not) ->
+ let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
+ | [|a;b|] when eq_constr l (Lazy.force coq_iff) ->
let f,env,tg = xparse_formula env tg a in
let g,env,tg = xparse_formula env tg b in
- mkformula_binary mkI term f g,env,tg
+ mkformula_binary mkIff term f g,env,tg
+ | _ -> parse_atom env tg term)
+ | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)->
+ let f,env,tg = xparse_formula env tg a in
+ let g,env,tg = xparse_formula env tg b in
+ mkformula_binary mkI term f g,env,tg
| _ when eq_constr term (Lazy.force coq_True) -> (TT,env,tg)
| _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg)
- | _ -> X(term),env,tg in
+ | _ when is_prop term -> X(term),env,tg
+ | _ -> raise ParseError
+ in
xparse_formula env tg ((*Reductionops.whd_zeta*) term)
let dump_formula typ dump_atom f =
@@ -1162,12 +1245,214 @@ struct
| X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|]) in
xdump f
- (**
- * Given a conclusion and a list of affectations, rebuild a term prefixed by
- * the appropriate letins.
- * TODO: reverse the list of bindings!
- *)
+ let prop_env_of_formula form =
+ let rec doit env = function
+ | TT | FF | A(_,_,_) -> env
+ | X t -> fst (Env.compute_rank_add env t)
+ | C(f1,f2) | D(f1,f2) | I(f1,_,f2) ->
+ doit (doit env f1) f2
+ | N f -> doit env f in
+
+ doit [] form
+
+ let var_env_of_formula form =
+
+ let rec vars_of_expr = function
+ | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n)
+ | Mc.PEc z -> ISet.empty
+ | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) ->
+ ISet.union (vars_of_expr e1) (vars_of_expr e2)
+ | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e
+ in
+
+ let vars_of_atom {Mc.flhs ; Mc.fop; Mc.frhs} =
+ ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in
+
+ let rec doit = function
+ | TT | FF | X _ -> ISet.empty
+ | A (a,t,c) -> vars_of_atom a
+ | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2)
+ | N f -> doit f in
+
+ doit form
+
+
+
+
+ type 'cst dump_expr = (* 'cst is the type of the syntactic constants *)
+ {
+ interp_typ : constr;
+ dump_cst : 'cst -> constr;
+ dump_add : constr;
+ dump_sub : constr;
+ dump_opp : constr;
+ dump_mul : constr;
+ dump_pow : constr;
+ dump_pow_arg : Mc.n -> constr;
+ dump_op : (Mc.op2 * Term.constr) list
+ }
+
+let dump_zexpr = lazy
+ {
+ interp_typ = Lazy.force coq_Z;
+ dump_cst = dump_z;
+ dump_add = Lazy.force coq_Zplus;
+ dump_sub = Lazy.force coq_Zminus;
+ dump_opp = Lazy.force coq_Zopp;
+ dump_mul = Lazy.force coq_Zmult;
+ dump_pow = Lazy.force coq_Zpower;
+ dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+ dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table
+ }
+
+let dump_qexpr = lazy
+ {
+ interp_typ = Lazy.force coq_Q;
+ dump_cst = dump_q;
+ dump_add = Lazy.force coq_Qplus;
+ dump_sub = Lazy.force coq_Qminus;
+ dump_opp = Lazy.force coq_Qopp;
+ dump_mul = Lazy.force coq_Qmult;
+ dump_pow = Lazy.force coq_Qpower;
+ dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+ dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table
+ }
+
+ let dump_positive_as_R p =
+ let mult = Lazy.force coq_Rmult in
+ let add = Lazy.force coq_Rplus in
+
+ let one = Lazy.force coq_R1 in
+ let mk_add x y = mkApp(add,[|x;y|]) in
+ let mk_mult x y = mkApp(mult,[|x;y|]) in
+
+ let two = mk_add one one in
+
+ let rec dump_positive p =
+ match p with
+ | Mc.XH -> one
+ | Mc.XO p -> mk_mult two (dump_positive p)
+ | Mc.XI p -> mk_add one (mk_mult two (dump_positive p)) in
+
+ dump_positive p
+
+let dump_n_as_R n =
+ let z = CoqToCaml.n n in
+ if z = 0
+ then Lazy.force coq_R0
+ else dump_positive_as_R (CamlToCoq.positive z)
+
+
+let rec dump_Rcst_as_R cst =
+ match cst with
+ | Mc.C0 -> Lazy.force coq_R0
+ | Mc.C1 -> Lazy.force coq_R1
+ | Mc.CQ q -> Term.mkApp(Lazy.force coq_IQR, [| dump_q q |])
+ | Mc.CZ z -> Term.mkApp(Lazy.force coq_IZR, [| dump_z z |])
+ | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+ | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+ | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+ | Mc.CInv t -> Term.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |])
+ | Mc.COpp t -> Term.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |])
+
+
+let dump_rexpr = lazy
+ {
+ interp_typ = Lazy.force coq_R;
+ dump_cst = dump_Rcst_as_R;
+ dump_add = Lazy.force coq_Rplus;
+ dump_sub = Lazy.force coq_Rminus;
+ dump_opp = Lazy.force coq_Ropp;
+ dump_mul = Lazy.force coq_Rmult;
+ dump_pow = Lazy.force coq_Rpower;
+ dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)));
+ dump_op = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table
+ }
+
+
+
+
+(** [make_goal_of_formula depxr vars props form] where
+ - vars is an environment for the arithmetic variables occuring in form
+ - props is an environment for the propositions occuring in form
+ @return a goal where all the variables and propositions of the formula are quantified
+
+*)
+
+let rec make_goal_of_formula dexpr form =
+
+ let vars_idx =
+ List.mapi (fun i v -> (v, i+1)) (ISet.elements (var_env_of_formula form)) in
+
+ (* List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*)
+
+ let props = prop_env_of_formula form in
+
+ let vars_n = List.map (fun (_,i) -> (Names.id_of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in
+ let props_n = List.mapi (fun i _ -> (Names.id_of_string (Printf.sprintf "__p%i" (i+1))) , Term.mkProp) props in
+
+ let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in
+
+ let dump_expr i e =
+ let rec dump_expr = function
+ | Mc.PEX n -> mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx))
+ | Mc.PEc z -> dexpr.dump_cst z
+ | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add,
+ [| dump_expr e1;dump_expr e2|])
+ | Mc.PEsub(e1,e2) -> mkApp(dexpr.dump_sub,
+ [| dump_expr e1;dump_expr e2|])
+ | Mc.PEopp e -> mkApp(dexpr.dump_opp,
+ [| dump_expr e|])
+ | Mc.PEmul(e1,e2) -> mkApp(dexpr.dump_mul,
+ [| dump_expr e1;dump_expr e2|])
+ | Mc.PEpow(e,n) -> mkApp(dexpr.dump_pow,
+ [| dump_expr e; dexpr.dump_pow_arg n|])
+ in dump_expr e in
+
+ let mkop op e1 e2 =
+ try
+ Term.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|])
+ with Not_found ->
+ Term.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in
+
+ let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } =
+ mkop fop (dump_expr i flhs) (dump_expr i frhs) in
+
+ let rec xdump pi xi f =
+ match f with
+ | TT -> Lazy.force coq_True
+ | FF -> Lazy.force coq_False
+ | C(x,y) -> mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|])
+ | D(x,y) -> mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|])
+ | I(x,_,y) -> mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y)
+ | N(x) -> mkArrow (xdump pi xi x) (Lazy.force coq_False)
+ | A(x,_,_) -> dump_cstr xi x
+ | X(t) -> let idx = Env.get_rank props t in
+ mkRel (pi+idx) in
+
+ let nb_vars = List.length vars_n in
+ let nb_props = List.length props_n in
+
+ (* Printf.fprintf stdout "NBProps : %i\n" nb_props ;*)
+
+ let subst_prop p =
+ let idx = Env.get_rank props p in
+ mkVar (Names.id_of_string (Printf.sprintf "__p%i" idx)) in
+
+ let form' = map_prop subst_prop form in
+
+ (Term.prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n)
+ (Term.prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n)
+ (xdump (List.length vars_n) 0 form)),
+ List.rev props_n, List.rev var_name_pos,form')
+
+ (**
+ * Given a conclusion and a list of affectations, rebuild a term prefixed by
+ * the appropriate letins.
+ * TODO: reverse the list of bindings!
+ *)
+
let set l concl =
let rec xset acc = function
| [] -> acc
@@ -1242,29 +1527,25 @@ let coq_Empty = lazy
(Coqlib.gen_constant_in_modules "VarMap"
[["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
-let btree_of_array typ a =
- let size_of_a = Array.length a in
- let semi_size_of_a = size_of_a lsr 1 in
- let node = Lazy.force coq_Node
- and leaf = Lazy.force coq_Leaf
- and empty = Term.mkApp (Lazy.force coq_Empty, [| typ |]) in
- let rec aux n =
- if n > size_of_a
- then empty
- else if n > semi_size_of_a
- then Term.mkApp (leaf, [| typ; a.(n-1) |])
- else Term.mkApp (node, [| typ; aux (2*n); a.(n-1); aux (2*n+1) |])
- in
- aux 1
-
-let btree_of_array typ a =
- try
- btree_of_array typ a
- with x when Errors.noncritical x ->
- failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
-
-let dump_varmap typ env =
- btree_of_array typ (Array.of_list env)
+let coq_VarMap = lazy
+ (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
+
+
+let rec dump_varmap typ m =
+ match m with
+ | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |])
+ | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+ | Mc.Node(l,o,r) ->
+ Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+
+
+let vm_of_list env =
+ match env with
+ | [] -> Mc.Empty
+ | (d,_)::_ ->
+ List.fold_left (fun vm (c,i) ->
+ Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env
let rec pp_varmap o vm =
@@ -1329,7 +1610,7 @@ let rec parse_hyps gl parse_arith env tg hyps =
try
let (c,env,tg) = parse_formula gl parse_arith env tg t in
((i,c)::lhyps, env,tg)
- with e when Errors.noncritical e -> (lhyps,env,tg)
+ with e when CErrors.noncritical e -> (lhyps,env,tg)
(*(if debug then Printf.printf "parse_arith : %s\n" x);*)
@@ -1377,50 +1658,81 @@ let rcst_domain_spec = lazy {
dump_proof = dump_psatz coq_Q dump_q
}
+open Proofview.Notations
+
+(** Naive topological sort of constr according to the subterm-ordering *)
+
+(* An element is minimal x is minimal w.r.t y if
+ x <= y or (x and y are incomparable) *)
+
+let is_min le x y =
+ if le x y then true
+ else if le y x then false else true
+
+let is_minimal le l c = List.for_all (is_min le c) l
+
+let find_rem p l =
+ let rec xfind_rem acc l =
+ match l with
+ | [] -> (None, acc)
+ | x :: l -> if p x then (Some x, acc @ l)
+ else xfind_rem (x::acc) l in
+ xfind_rem [] l
+
+let find_minimal le l = find_rem (is_minimal le l) l
+
+let rec mk_topo_order le l =
+ match find_minimal le l with
+ | (None , _) -> []
+ | (Some v,l') -> v :: (mk_topo_order le l')
+
+
+let topo_sort_constr l = mk_topo_order Termops.dependent l
+
+
(**
* Instanciate the current Coq goal with a Micromega formula, a varmap, and a
* witness.
*)
-
-
-let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic =
- let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in
+let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) =
+ (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
- let vm = dump_varmap (spec.typ) env in
- (* todo : directly generate the proof term - or generalize befor conversion? *)
- Tacticals.tclTHENSEQ [
- (fun gl ->
- Proofview.V82.of_tactic (Tactics.change_concl
- (set
- [
- ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
- ("__varmap", vm, Term.mkApp
- (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|]));
- ("__wit", cert, cert_typ)
- ]
- (Tacmach.pf_concl gl))) gl);
- Tactics.generalize env ;
- Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ;
- ]
-
+ let vm = dump_varmap (spec.typ) (vm_of_list env) in
+ (* todo : directly generate the proof term - or generalize before conversion? *)
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let gl = Tacmach.New.of_old (fun x -> x) gl in
+ Tacticals.New.tclTHENLIST
+ [
+ Tactics.change_concl
+ (set
+ [
+ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+ ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
+ ("__wit", cert, cert_typ)
+ ]
+ (Tacmach.pf_concl gl))
+ ]
+ end }
(**
* The datastructures that aggregate prover attributes.
*)
-type ('a,'prf) prover = {
+type ('option,'a,'prf) prover = {
name : string ; (* name of the prover *)
- prover : 'a list -> 'prf option ; (* the prover itself *)
+ get_option : unit ->'option ; (* find the options of the prover *)
+ prover : 'option * 'a list -> 'prf option ; (* the prover itself *)
hyps : 'prf -> 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)*)
}
+
+
(**
* Given a list of provers and a disjunction of atoms, find a proof of any of
* the atoms. Returns an (optional) pair of a proof and a prover
@@ -1430,7 +1742,7 @@ type ('a,'prf) prover = {
let find_witness provers polys1 =
let provers = List.map (fun p ->
(fun l ->
- match p.prover l with
+ match p.prover (p.get_option (),l) with
| None -> None
| Some prf -> Some(prf,p)) , p.name) provers in
try_any provers (List.map fst polys1)
@@ -1482,10 +1794,10 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
(pp_ml_list prover.pp_f) (List.map fst new_cl) ;
flush stdout
end ; *)
- let res = try prover.compact prf remap with x when Errors.noncritical x ->
+ let res = try prover.compact prf remap with x when CErrors.noncritical x ->
if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
(* This should not happen -- this is the recovery plan... *)
- match prover.prover (List.map fst new_cl) with
+ match prover.prover (prover.get_option () ,List.map fst new_cl) with
| None -> failwith "proof compaction error"
| Some p -> p
in
@@ -1562,6 +1874,7 @@ let rec abstract_wrt_formula f1 f2 =
exception CsdpNotFound
+
(**
* This is the core of Micromega: apply the prover, analyze the result and
* prune unused fomulas, and finally modify the proof state.
@@ -1586,12 +1899,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "Formula....\n") ;
+ Feedback.msg_notice (Pp.str "Formula....\n") ;
let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ Feedback.msg_notice (Printer.prterm ff);
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
match witness_list_tags prover cnf_ff with
@@ -1611,11 +1924,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "\nAFormula\n") ;
+ Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Feedback.msg_notice (Printer.prterm ff');
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
@@ -1646,58 +1959,103 @@ let micromega_gen
(negate:'cst atom -> 'cst mc_cnf)
(normalise:'cst atom -> 'cst mc_cnf)
unsat deduce
- spec prover gl =
- let concl = Tacmach.pf_concl gl in
- let hyps = Tacmach.pf_hyps_types gl in
- try
- let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
- let env = Env.elements env in
- let spec = Lazy.force spec in
-
+ spec dumpexpr prover tac =
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let gl = Tacmach.New.of_old (fun x -> x) gl in
+ let concl = Tacmach.pf_concl gl in
+ let hyps = Tacmach.pf_hyps_types gl in
+ try
+ let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+ let env = Env.elements env in
+ let spec = Lazy.force spec in
+ let dumpexpr = Lazy.force dumpexpr in
+
match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with
- | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl
- | Some (ids,ff',res') ->
- (Tacticals.tclTHENSEQ
- [
- Tactics.generalize (List.map Term.mkVar ids) ;
- micromega_order_change spec res'
- (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
- ]) gl
- with
- | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
- Tacticals.tclFAIL 0 (Pp.str
- (" Skipping what remains of this tactic: the complexity of the goal requires "
- ^ "the use of a specialized external tool called csdp. \n\n"
- ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
- ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl
-
-
-
-let micromega_order_changer cert env ff gl =
+ | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
+ | Some (ids,ff',res') ->
+ let (arith_goal,props,vars,ff_arith) = make_goal_of_formula dumpexpr ff' in
+ let intro (id,_) = Tactics.introduction id in
+
+ let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+ let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+ let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+ let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+ let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in
+
+ let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
+ micromega_order_change spec res'
+ (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in
+
+ let goal_props = List.rev (prop_env_of_formula ff') in
+
+ let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in
+
+ let arith_args = goal_props @ goal_vars in
+
+ let kill_arith =
+ Tacticals.New.tclTHEN
+ (Tactics.keep [])
+ ((*Tactics.tclABSTRACT None*)
+ (Tacticals.New.tclTHEN tac_arith tac)) in
+
+ Tacticals.New.tclTHENS
+ (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+ [
+ kill_arith;
+ (Tacticals.New.tclTHENLIST
+ [(Tactics.generalize (List.map Term.mkVar ids));
+ Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+ ] )
+ ]
+ with
+ | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+ | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+ | CsdpNotFound -> flush stdout ;
+ Tacticals.New.tclFAIL 0 (Pp.str
+ (" Skipping what remains of this tactic: the complexity of the goal requires "
+ ^ "the use of a specialized external tool called csdp. \n\n"
+ ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+ ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+ end }
+
+let micromega_gen parse_arith
+ (negate:'cst atom -> 'cst mc_cnf)
+ (normalise:'cst atom -> 'cst mc_cnf)
+ unsat deduce
+ spec prover =
+ (micromega_gen parse_arith negate normalise unsat deduce spec prover)
+
+
+
+let micromega_order_changer cert env ff =
+ (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
let coeff = Lazy.force coq_Rcst in
let dump_coeff = dump_Rcst in
let typ = Lazy.force coq_R in
let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
-
- let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
- let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
- let vm = dump_varmap (typ) env in
- Proofview.V82.of_tactic (Tactics.change_concl
- (set
+
+ let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
+ let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
+ let vm = dump_varmap (typ) (vm_of_list env) in
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let gl = Tacmach.New.of_old (fun x -> x) gl in
+ Tacticals.New.tclTHENLIST
[
- ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
- ("__varmap", vm, Term.mkApp
- (Coqlib.gen_constant_in_modules "VarMap"
- [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
- ("__wit", cert, cert_typ)
+ (Tactics.change_concl
+ (set
+ [
+ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+ ("__varmap", vm, Term.mkApp
+ (Coqlib.gen_constant_in_modules "VarMap"
+ [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
+ ("__wit", cert, cert_typ)
+ ]
+ (Tacmach.pf_concl gl)));
+ (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*)
]
- (Tacmach.pf_concl gl)
- ))
- gl
-
+ end }
-let micromega_genr prover gl =
+let micromega_genr prover tac =
let parse_arith = parse_rarith in
let negate = Mc.rnegate in
let normalise = Mc.rnormalise in
@@ -1710,41 +2068,77 @@ let micromega_genr prover gl =
proof_typ = Lazy.force coq_QWitness ;
dump_proof = dump_psatz coq_Q dump_q
} in
-
- let concl = Tacmach.pf_concl gl in
- let hyps = Tacmach.pf_hyps_types gl in
- try
- let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
- let env = Env.elements env in
- let spec = Lazy.force spec in
-
- let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
- let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
-
- match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with
- | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let gl = Tacmach.New.of_old (fun x -> x) gl in
+ let concl = Tacmach.pf_concl gl in
+ let hyps = Tacmach.pf_hyps_types gl in
+
+ try
+ let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+ let env = Env.elements env in
+ let spec = Lazy.force spec in
+
+ let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
+ let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
+
+ match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with
+ | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
| Some (ids,ff',res') ->
- let (ff,ids') = formula_hyps_concl
+ let (ff,ids) = formula_hyps_concl
(List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
+ let ff' = abstract_wrt_formula ff' ff in
+
+ let (arith_goal,props,vars,ff_arith) = make_goal_of_formula (Lazy.force dump_rexpr) ff' in
+ let intro (id,_) = Tactics.introduction id in
+
+ let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+ let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+ let ipat_of_name id = Some (Loc.ghost, Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+ let goal_name = Tactics.fresh_id [] (Names.Id.of_string "__arith") gl in
+ let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in
+
+ let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
+ micromega_order_changer res' env' ff_arith ] in
+
+ let goal_props = List.rev (prop_env_of_formula ff') in
+
+ let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in
+
+ let arith_args = goal_props @ goal_vars in
+
+ let kill_arith =
+ Tacticals.New.tclTHEN
+ (Tactics.keep [])
+ ((*Tactics.tclABSTRACT None*)
+ (Tacticals.New.tclTHEN tac_arith tac)) in
- (Tacticals.tclTHENSEQ
- [
- Tactics.generalize (List.map Term.mkVar ids) ;
- micromega_order_changer res' env (abstract_wrt_formula ff' ff)
- ]) gl
- with
- | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
- Tacticals.tclFAIL 0 (Pp.str
- (" Skipping what remains of this tactic: the complexity of the goal requires "
- ^ "the use of a specialized external tool called csdp. \n\n"
- ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
- ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl
+ Tacticals.New.tclTHENS
+ (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+ [
+ kill_arith;
+ (Tacticals.New.tclTHENLIST
+ [(Tactics.generalize (List.map Term.mkVar ids));
+ Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+ ] )
+ ]
+ with
+ | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+ | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+ | CsdpNotFound -> flush stdout ;
+ Tacticals.New.tclFAIL 0 (Pp.str
+ (" Skipping what remains of this tactic: the complexity of the goal requires "
+ ^ "the use of a specialized external tool called csdp. \n\n"
+ ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+ ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+ end }
+let micromega_genr prover = (micromega_genr prover)
+
+
let lift_ratproof prover l =
match prover l with
| None -> None
@@ -1766,7 +2160,7 @@ module Cache = PHashtable(struct
let hash = Hashtbl.hash
end)
-let csdp_cache = "csdp.cache"
+let csdp_cache = ".csdp.cache"
(**
* Build the command to call csdpcert, and launch it. This in turn will call
@@ -1818,7 +2212,7 @@ let call_csdpcert_q provername poly =
let cert = Certificate.q_cert_of_pos cert in
if Mc.qWeakChecker poly cert
then Some cert
- else ((print_string "buggy certificate" ; flush stdout) ;None)
+ else ((print_string "buggy certificate") ;None)
let call_csdpcert_z provername poly =
let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
@@ -1898,38 +2292,61 @@ let compact_pt pt f =
let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l)
-let linear_prover_Z = {
- name = "linear prover" ;
- prover = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ;
- hyps = hyps_of_pt ;
- compact = compact_pt ;
- pp_prf = pp_proof_term;
- pp_f = fun o x -> pp_pol pp_z o (fst x)
-}
+module CacheZ = PHashtable(struct
+ type prover_option = bool * int
+
+ type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list)
+ let equal = (=)
+ let hash = Hashtbl.hash
+end)
+module CacheQ = PHashtable(struct
+ type t = int * ((Mc.q Mc.pol * Mc.op1) list)
+ let equal = (=)
+ let hash = Hashtbl.hash
+end)
+
+let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+
+
+
let linear_prover_Q = {
- name = "linear prover";
- prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
- hyps = hyps_of_cone ;
- compact = compact_cone ;
- pp_prf = pp_psatz pp_q ;
- pp_f = fun o x -> pp_pol pp_q o (fst x)
+ name = "linear prover";
+ get_option = get_lra_option ;
+ prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
+ hyps = hyps_of_cone ;
+ compact = compact_cone ;
+ pp_prf = pp_psatz pp_q ;
+ pp_f = fun o x -> pp_pol pp_q o (fst x)
}
let linear_prover_R = {
name = "linear prover";
- prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
+ get_option = get_lra_option ;
+ prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
hyps = hyps_of_cone ;
compact = compact_cone ;
pp_prf = pp_psatz pp_q ;
pp_f = fun o x -> pp_pol pp_q o (fst x)
}
+let nlinear_prover_R = {
+ name = "nra";
+ get_option = get_lra_option;
+ prover = memo_nra ;
+ hyps = hyps_of_cone ;
+ compact = compact_cone ;
+ pp_prf = pp_psatz pp_q ;
+ pp_f = fun o x -> pp_pol pp_q o (fst x)
+}
let non_linear_prover_Q str o = {
name = "real nonlinear prover";
- prover = call_csdpcert_q (str, o);
+ get_option = (fun () -> (str,o));
+ prover = (fun (o,l) -> call_csdpcert_q o l);
hyps = hyps_of_cone;
compact = compact_cone ;
pp_prf = pp_psatz pp_q ;
@@ -1938,7 +2355,8 @@ let non_linear_prover_Q str o = {
let non_linear_prover_R str o = {
name = "real nonlinear prover";
- prover = call_csdpcert_q (str, o);
+ get_option = (fun () -> (str,o));
+ prover = (fun (o,l) -> call_csdpcert_q o l);
hyps = hyps_of_cone;
compact = compact_cone;
pp_prf = pp_psatz pp_q;
@@ -1947,30 +2365,18 @@ let non_linear_prover_R str o = {
let non_linear_prover_Z str o = {
name = "real nonlinear prover";
- prover = lift_ratproof (call_csdpcert_z (str, o));
+ get_option = (fun () -> (str,o));
+ prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l);
hyps = hyps_of_pt;
compact = compact_pt;
pp_prf = pp_proof_term;
pp_f = fun o x -> pp_pol pp_z o (fst x)
}
-module CacheZ = PHashtable(struct
- type t = (Mc.z Mc.pol * Mc.op1) list
- let equal = Pervasives.(=)
- let hash = Hashtbl.hash
-end)
-
-let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia)
-let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia)
-
-(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*)
-(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*)
-
-
-
let linear_Z = {
name = "lia";
- prover = memo_zlinear_prover ;
+ get_option = get_lia_option;
+ prover = memo_zlinear_prover ;
hyps = hyps_of_pt;
compact = compact_pt;
pp_prf = pp_proof_term;
@@ -1979,7 +2385,8 @@ let linear_Z = {
let nlinear_Z = {
name = "nlia";
- prover = memo_nlia ;
+ get_option = get_lia_option;
+ prover = memo_nlia ;
hyps = hyps_of_pt;
compact = compact_pt;
pp_prf = pp_proof_term;
@@ -2001,57 +2408,53 @@ let tauto_lia ff =
* solvers
*)
-let psatzl_Z gl =
- micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
- [ linear_prover_Z ] gl
-
-let psatzl_Q gl =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
- [ linear_prover_Q ] gl
-
-let psatz_Q i gl =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
- [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl
+let lra_Q =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+ [ linear_prover_Q ]
+let psatz_Q i =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+ [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
-let psatzl_R gl =
- micromega_genr [ linear_prover_R ] gl
+let lra_R =
+ micromega_genr [ linear_prover_R ]
+let psatz_R i =
+ micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ]
-let psatz_R i gl =
- micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl
+let psatz_Z i =
+ micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+ [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ]
-let psatz_Z i gl =
- micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
- [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl
+let sos_Z =
+ micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+ [ non_linear_prover_Z "pure_sos" None ]
-let sos_Z gl =
- micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
- [ non_linear_prover_Z "pure_sos" None ] gl
+let sos_Q =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+ [ non_linear_prover_Q "pure_sos" None ]
-let sos_Q gl =
- micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
- [ non_linear_prover_Q "pure_sos" None ] gl
+let sos_R =
+ micromega_genr [ non_linear_prover_R "pure_sos" None ]
-let sos_R gl =
- micromega_genr [ non_linear_prover_R "pure_sos" None ] gl
+let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+ [ linear_Z ]
-let xlia gl =
- try
- micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
- [ linear_Z ] gl
- with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
+let xnlia =
+ micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+ [ nlinear_Z ]
-let xnlia gl =
- try
- micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
- [ nlinear_Z ] gl
- with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
+let nra =
+ micromega_genr [ nlinear_prover_R ]
+let nqa =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+ [ nlinear_prover_R ]
+
(* Local Variables: *)
(* coding: utf-8 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 09:35:11 +0000