aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/ZifyBool.v8
-rw-r--r--plugins/micromega/ZifyInst.v64
-rw-r--r--plugins/micromega/certificate.ml66
-rw-r--r--plugins/micromega/csdpcert.ml20
-rw-r--r--plugins/micromega/g_micromega.mlg2
-rw-r--r--plugins/micromega/mfourier.ml272
-rw-r--r--plugins/micromega/mutils.ml52
-rw-r--r--plugins/micromega/persistent_cache.ml80
-rw-r--r--plugins/micromega/sos_lib.ml16
9 files changed, 321 insertions, 259 deletions
diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v
index b94b74097b..4060478363 100644
--- a/plugins/micromega/ZifyBool.v
+++ b/plugins/micromega/ZifyBool.v
@@ -74,6 +74,14 @@ Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0).
Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0).
+Instance Op_isZero : UnOp isZero :=
+ { TUOp := isZero; TUOpInj := ltac: (reflexivity) }.
+Add UnOp Op_isZero.
+
+Instance Op_isLeZero : UnOp isLeZero :=
+ { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }.
+Add UnOp Op_isLeZero.
+
(* Some intermediate lemma *)
Lemma Z_eqb_isZero : forall n m,
diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v
index afd7101667..97f6fe0613 100644
--- a/plugins/micromega/ZifyInst.v
+++ b/plugins/micromega/ZifyInst.v
@@ -169,7 +169,7 @@ Add BinRel Op_eq_pos.
(* zify_positive_op *)
-Program Instance Op_Z_of_N : UnOp Z.of_N :=
+Instance Op_Z_of_N : UnOp Z.of_N :=
{ TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }.
Add UnOp Op_Z_of_N.
@@ -189,6 +189,10 @@ Instance Op_pos_succ : UnOp Pos.succ :=
{ TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }.
Add UnOp Op_pos_succ.
+Instance Op_pos_pred_double : UnOp Pos.pred_double :=
+ { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(reflexivity) }.
+Add UnOp Op_pos_pred_double.
+
Instance Op_pos_pred : UnOp Pos.pred :=
{ TUOp := fun x => Z.max 1 (x - 1) ;
TUOpInj := ltac :
@@ -197,14 +201,30 @@ Instance Op_pos_pred : UnOp Pos.pred :=
apply Pos2Z.inj_sub_max) }.
Add UnOp Op_pos_pred.
+Instance Op_pos_predN : UnOp Pos.pred_N :=
+ { TUOp := fun x => x - 1 ;
+ TUOpInj := ltac: (now destruct x; rewrite N.pos_pred_spec) }.
+Add UnOp Op_pos_predN.
+
Instance Op_pos_of_succ_nat : UnOp Pos.of_succ_nat :=
{ TUOp := fun x => x + 1 ; TUOpInj := Zpos_P_of_succ_nat }.
Add UnOp Op_pos_of_succ_nat.
-Program Instance Op_pos_add : BinOp Pos.add :=
+Instance Op_pos_of_nat : UnOp Pos.of_nat :=
+ { TUOp := fun x => Z.max 1 x ;
+ TUOpInj := ltac: (now destruct x;
+ [|rewrite <- Pos.of_nat_succ, <- (Nat2Z.inj_max 1)]) }.
+Add UnOp Op_pos_of_nat.
+
+Instance Op_pos_add : BinOp Pos.add :=
{ TBOp := Z.add ; TBOpInj := ltac: (reflexivity) }.
Add BinOp Op_pos_add.
+Instance Op_pos_add_carry : BinOp Pos.add_carry :=
+ { TBOp := fun x y => x + y + 1 ;
+ TBOpInj := ltac:(now intros; rewrite Pos.add_carry_spec, Pos2Z.inj_succ) }.
+Add BinOp Op_pos_add_carry.
+
Instance Op_pos_sub : BinOp Pos.sub :=
{ TBOp := fun n m => Z.max 1 (n - m) ;TBOpInj := Pos2Z.inj_sub_max }.
Add BinOp Op_pos_sub.
@@ -221,6 +241,14 @@ Instance Op_pos_max : BinOp Pos.max :=
{ TBOp := Z.max ; TBOpInj := Pos2Z.inj_max }.
Add BinOp Op_pos_max.
+Instance Op_pos_pow : BinOp Pos.pow :=
+ { TBOp := Z.pow ; TBOpInj := Pos2Z.inj_pow }.
+Add BinOp Op_pos_pow.
+
+Instance Op_pos_square : UnOp Pos.square :=
+ { TUOp := Z.square ; TUOpInj := Pos2Z.inj_square }.
+Add UnOp Op_pos_square.
+
Instance Op_xO : UnOp xO :=
{ TUOp := fun x => 2 * x ; TUOpInj := ltac: (reflexivity) }.
Add UnOp Op_xO.
@@ -295,8 +323,6 @@ Instance Op_N_div : BinOp N.div :=
{| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}.
Add BinOp Op_N_div.
-
-
Instance Op_N_mod : BinOp N.modulo :=
{| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}.
Add BinOp Op_N_mod.
@@ -390,10 +416,38 @@ Instance Op_Z_sgn : UnOp Z.sgn :=
{ TUOp := Z.sgn ; TUOpInj := ltac:(reflexivity) }.
Add UnOp Op_Z_sgn.
+Instance Op_Z_pow : BinOp Z.pow :=
+ { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }.
+Add BinOp Op_Z_pow.
+
Instance Op_Z_pow_pos : BinOp Z.pow_pos :=
{ TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }.
Add BinOp Op_Z_pow_pos.
+Instance Op_Z_double : UnOp Z.double :=
+ { TUOp := Z.mul 2 ; TUOpInj := Z.double_spec }.
+Add UnOp Op_Z_double.
+
+Instance Op_Z_pred_double : UnOp Z.pred_double :=
+ { TUOp := fun x => 2 * x - 1 ; TUOpInj := Z.pred_double_spec }.
+Add UnOp Op_Z_pred_double.
+
+Instance Op_Z_succ_double : UnOp Z.succ_double :=
+ { TUOp := fun x => 2 * x + 1 ; TUOpInj := Z.succ_double_spec }.
+Add UnOp Op_Z_succ_double.
+
+Instance Op_Z_square : UnOp Z.square :=
+ { TUOp := fun x => x * x ; TUOpInj := Z.square_spec }.
+Add UnOp Op_Z_square.
+
+Instance Op_Z_div2 : UnOp Z.div2 :=
+ { TUOp := fun x => x / 2 ; TUOpInj := Z.div2_div }.
+Add UnOp Op_Z_div2.
+
+Instance Op_Z_quot2 : UnOp Z.quot2 :=
+ { TUOp := fun x => Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }.
+Add UnOp Op_Z_quot2.
+
Lemma of_nat_to_nat_eq : forall x, Z.of_nat (Z.to_nat x) = Z.max 0 x.
Proof.
destruct x.
@@ -435,7 +489,7 @@ Proof.
Qed.
-Program Instance ZminSpec : BinOpSpec Z.min :=
+Instance ZminSpec : BinOpSpec Z.min :=
{| BPred := fun n m r => n < m /\ r = n \/ m <= n /\ r = m ;
BSpec := Z.min_spec |}.
Add Spec ZminSpec.
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 24039c93c6..82c2be582b 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -96,7 +96,7 @@ let rec fixpoint f x =
if (=) y' x then y'
else fixpoint f y'
-let rec_simpl_cone n_spec e =
+let rec_simpl_cone n_spec e =
let simpl_cone =
Mc.simpl_cone n_spec.zero n_spec.unit n_spec.mult n_spec.eqb in
@@ -107,21 +107,21 @@ let rec_simpl_cone n_spec e =
simpl_cone (Mc.PsatzAdd (rec_simpl_cone t1, rec_simpl_cone t2))
| x -> simpl_cone x in
rec_simpl_cone e
-
-
+
+
let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c
-(* The binding with Fourier might be a bit obsolete
+(* The binding with Fourier might be a bit obsolete
-- how does it handle equalities ? *)
(* Certificates are elements of the cone such that P = 0 *)
(* To begin with, we search for certificates of the form:
- a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0
+ a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0
where pi >= 0 qi > 0
- ai >= 0
+ ai >= 0
bi >= 0
Sum bi + c >= 1
This is a linear problem: each monomial is considered as a variable.
@@ -135,7 +135,7 @@ let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c
let constrain_variable v l =
let coeffs = List.fold_left (fun acc p -> (Vect.get v p.coeffs)::acc) [] l in
{ coeffs = Vect.from_list ((Big_int zero_big_int):: (Big_int zero_big_int):: (List.rev coeffs)) ;
- op = Eq ;
+ op = Eq ;
cst = Big_int zero_big_int }
@@ -143,10 +143,10 @@ let constrain_variable v l =
let constrain_constant l =
let coeffs = List.fold_left (fun acc p -> minus_num p.cst ::acc) [] l in
{ coeffs = Vect.from_list ((Big_int zero_big_int):: (Big_int unit_big_int):: (List.rev coeffs)) ;
- op = Eq ;
+ op = Eq ;
cst = Big_int zero_big_int }
-let positivity l =
+let positivity l =
let rec xpositivity i l =
match l with
| [] -> []
@@ -169,7 +169,7 @@ let cstr_of_poly (p,o) =
let variables_of_cstr c = Vect.variables c.coeffs
-(* If the certificate includes at least one strict inequality,
+(* If the certificate includes at least one strict inequality,
the obtained polynomial can also be 0 *)
let build_dual_linear_system l =
@@ -486,7 +486,7 @@ let square_of_var i =
let x = LinPoly.var i in
((LinPoly.product x x,Ge),(ProofFormat.Square x))
-
+
(** [nlinear_preprocess sys] augments the system [sys] by performing some limited non-linear reasoning.
For instance, it asserts that the x² ≥0 but also that if c₁ ≥ 0 ∈ sys and c₂ ≥ 0 ∈ sys then c₁ × c₂ ≥ 0.
The resulting system is linearised.
@@ -510,7 +510,7 @@ let nlinear_preprocess (sys:WithProof.t list) =
let sys = ISet.fold (fun i acc -> square_of_var i :: acc) collect_vars sys in
let sys = sys @ (all_pairs WithProof.product sys) in
-
+
if debug then begin
Printf.fprintf stdout "Preprocessed\n";
List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys;
@@ -545,12 +545,12 @@ let linear_prover_with_cert prfdepth sys =
| Some cert ->
Prf (ProofFormat.cmpl_prf_rule Mc.normQ CamlToCoq.q (List.mapi (fun i e -> i) sys) cert)
-(* The prover is (probably) incomplete --
+(* The prover is (probably) incomplete --
only searching for naive cutting planes *)
open Sos_types
-let rec scale_term t =
+let rec scale_term t =
match t with
| Zero -> unit_big_int , Zero
| Const n -> (denominator n) , Const (Big_int (numerator n))
@@ -564,7 +564,7 @@ let rec scale_term t =
if Int.equal (compare_big_int e unit_big_int) 0
then (unit_big_int, Add (y1,y2))
else e, Add (Mul(Const (Big_int s2'), y1),
- Mul (Const (Big_int s1'), y2))
+ Mul (Const (Big_int s1'), y2))
| Sub _ -> failwith "scale term: not implemented"
| Mul(y,z) -> let s1,y1 = scale_term y and s2,y2 = scale_term z in
mult_big_int s1 s2 , Mul (y1, y2)
@@ -615,14 +615,14 @@ let rec term_to_q_expr = function
let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e)
-let rec product l =
+let rec product l =
match l with
| [] -> Mc.PsatzZ
| [i] -> Mc.PsatzIn (Ml2C.nat i)
| i ::l -> Mc.PsatzMulE(Mc.PsatzIn (Ml2C.nat i), product l)
-let q_cert_of_pos pos =
+let q_cert_of_pos pos =
let rec _cert_of_pos = function
Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i)
| Axiom_le i -> Mc.PsatzIn (Ml2C.nat i)
@@ -651,7 +651,7 @@ let rec term_to_z_expr = function
let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e)
-let z_cert_of_pos pos =
+let z_cert_of_pos pos =
let s,pos = (scale_certificate pos) in
let rec _cert_of_pos = function
Axiom_eq i -> Mc.PsatzIn (Ml2C.nat i)
@@ -689,7 +689,7 @@ type prf_sys = (cstr * ProofFormat.prf_rule) list
(** Proof generating pivoting over variable v *)
-let pivot v (c1,p1) (c2,p2) =
+let pivot v (c1,p1) (c2,p2) =
let {coeffs = v1 ; op = op1 ; cst = n1} = c1
and {coeffs = v2 ; op = op2 ; cst = n2} = c2 in
@@ -726,7 +726,7 @@ let pivot v (c1,p1) (c2,p2) =
else None (* op2 could be Eq ... this might happen *)
-let simpl_sys sys =
+let simpl_sys sys =
List.fold_left (fun acc (c,p) ->
match check_int_sat (c,p) with
| Tauto -> acc
@@ -739,7 +739,7 @@ let simpl_sys sys =
[ext_gcd a b = (x,y,g)] iff [ax+by=g]
Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm
*)
-let rec ext_gcd a b =
+let rec ext_gcd a b =
if Int.equal (sign_big_int b) 0
then (unit_big_int,zero_big_int)
else
@@ -747,7 +747,7 @@ let rec ext_gcd a b =
let (s,t) = ext_gcd b r in
(t, sub_big_int s (mult_big_int q t))
-let extract_coprime (c1,p1) (c2,p2) =
+let extract_coprime (c1,p1) (c2,p2) =
if c1.op == Eq && c2.op == Eq
then Vect.exists2 (fun n1 n2 ->
Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0)
@@ -776,7 +776,7 @@ let extract_coprime_equation psys =
let pivot_sys v pc psys = apply_and_normalise check_int_sat (pivot v pc) psys
-let reduce_coprime psys =
+let reduce_coprime psys =
let oeq,sys = extract_coprime_equation psys in
match oeq with
| None -> None (* Nothing to do *)
@@ -793,7 +793,7 @@ let reduce_coprime psys =
Some (pivot_sys v (cstr,prf) ((c1,p1)::sys))
(** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *)
-let reduce_unary psys =
+let reduce_unary psys =
let is_unary_equation (cstr,prf) =
if cstr.op == Eq
then
@@ -807,7 +807,7 @@ let reduce_unary psys =
Some(pivot_sys v pc sys)
-let reduce_var_change psys =
+let reduce_var_change psys =
let rec rel_prime vect =
match Vect.choose vect with
@@ -854,7 +854,7 @@ let reduction_equations psys =
(** [get_bound sys] returns upon success an interval (lb,e,ub) with proofs *)
-let get_bound sys =
+let get_bound sys =
let is_small (v,i) =
match Itv.range i with
| None -> false
@@ -909,12 +909,12 @@ let get_bound sys =
| None -> None
-let check_sys sys =
+let check_sys sys =
List.for_all (fun (c,p) -> Vect.for_all (fun _ n -> sign_num n <> 0) c.coeffs) sys
open ProofFormat
-let xlia (can_enum:bool) reduction_equations sys =
+let xlia (can_enum:bool) reduction_equations sys =
let rec enum_proof (id:int) (sys:prf_sys) =
@@ -979,9 +979,9 @@ let xlia (can_enum:bool) reduction_equations sys =
end;
let prf = compile_proof env prf in
(*try
- if Mc.zChecker sys' prf then Some prf else
- raise Certificate.BadCertificate
- with Failure s -> (Printf.printf "%s" s ; Some prf)
+ if Mc.zChecker sys' prf then Some prf else
+ raise Certificate.BadCertificate
+ with Failure s -> (Printf.printf "%s" s ; Some prf)
*) Prf prf
let xlia_simplex env red sys =
@@ -1029,7 +1029,7 @@ let gen_bench (tac, prover) can_enum prfdepth sys =
end);
res
-let lia (can_enum:bool) (prfdepth:int) sys =
+let lia (can_enum:bool) (prfdepth:int) sys =
let sys = develop_constraints prfdepth z_spec sys in
if debug then begin
Printf.fprintf stdout "Input problem\n";
@@ -1049,7 +1049,7 @@ let lia (can_enum:bool) (prfdepth:int) sys =
let make_cstr_system sys =
List.map (fun ((p,o),prf) -> (cstr_of_poly (p,o), prf)) sys
-let nlia enum prfdepth sys =
+let nlia enum prfdepth sys =
let sys = develop_constraints prfdepth z_spec sys in
let is_linear = List.for_all (fun ((p,_),_) -> LinPoly.is_linear p) sys in
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index cf5f60fb55..09e354957a 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -62,9 +62,9 @@ let partition_expr l =
| Mc.Equal -> ((e,i)::eq,ge,neq)
| Mc.NonStrict -> (eq,(e,Axiom_le i)::ge,neq)
| Mc.Strict -> (* e > 0 == e >= 0 /\ e <> 0 *)
- (eq, (e,Axiom_lt i)::ge,(e,Axiom_lt i)::neq)
+ (eq, (e,Axiom_lt i)::ge,(e,Axiom_lt i)::neq)
| Mc.NonEqual -> (eq,ge,(e,Axiom_eq i)::neq)
- (* Not quite sure -- Coq interface has changed *)
+ (* Not quite sure -- Coq interface has changed *)
in f 0 l
@@ -72,7 +72,7 @@ let rec sets_of_list l =
match l with
| [] -> [[]]
| e::l -> let s = sets_of_list l in
- s@(List.map (fun s0 -> e::s0) s)
+ s@(List.map (fun s0 -> e::s0) s)
(* The exploration is probably not complete - for simple cases, it works... *)
let real_nonlinear_prover d l =
@@ -83,9 +83,9 @@ let real_nonlinear_prover d l =
let rec elim_const = function
[] -> []
| (x,y)::l -> let p = poly_of_term (expr_to_term x) in
- if poly_isconst p
- then elim_const l
- else (p,y)::(elim_const l) in
+ if poly_isconst p
+ then elim_const l
+ else (p,y)::(elim_const l) in
let eq = elim_const eq in
let peq = List.map fst eq in
@@ -104,7 +104,7 @@ let real_nonlinear_prover d l =
let (cert_ideal, cert_cone,monoid) = deepen_until d (fun d ->
tryfind (fun m -> let (ci,cc) =
real_positivnullstellensatz_general false d peq pge (poly_neg (fst m) ) in
- (ci,cc,snd m)) monoids) 0 in
+ (ci,cc,snd m)) monoids) 0 in
let proofs_ideal = List.map2 (fun q i -> Eqmul(term_of_poly q,Axiom_eq i))
cert_ideal (List.map snd eq) in
@@ -141,9 +141,9 @@ let pure_sos l =
let plt = poly_neg (poly_of_term (expr_to_term (fst lt))) in
let (n,polys) = sumofsquares plt in (* n * (ci * pi^2) *)
let pos = Product (Rational_lt n,
- List.fold_right (fun (c,p) rst -> Sum (Product (Rational_lt c, Square
- (term_of_poly p)), rst))
- polys (Rational_lt (Int 0))) in
+ List.fold_right (fun (c,p) rst -> Sum (Product (Rational_lt c, Square
+ (term_of_poly p)), rst))
+ polys (Rational_lt (Int 0))) in
let proof = Sum(Axiom_lt i, pos) in
(* let s,proof' = scale_certificate proof in
let cert = snd (cert_of_pos proof') in *)
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg
index bcf546f059..edf8106f30 100644
--- a/plugins/micromega/g_micromega.mlg
+++ b/plugins/micromega/g_micromega.mlg
@@ -56,7 +56,7 @@ TACTIC EXTEND NQA
END
-
+
TACTIC EXTEND Sos_Z
| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) }
END
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 943bcb384b..75cdfa24f1 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -71,13 +71,13 @@ exception SystemContradiction of proof
let pp_cstr o (vect,bnd) =
let (l,r) = bnd in
(match l with
- | None -> ()
- | Some n -> Printf.fprintf o "%s <= " (string_of_num n))
+ | None -> ()
+ | Some n -> Printf.fprintf o "%s <= " (string_of_num n))
;
Vect.pp o vect ;
(match r with
- | None -> output_string o"\n"
- | Some n -> Printf.fprintf o "<=%s\n" (string_of_num n))
+ | None -> output_string o"\n"
+ | Some n -> Printf.fprintf o "<=%s\n" (string_of_num n))
let pp_system o sys=
@@ -96,7 +96,7 @@ let merge_cstr_info i1 i2 =
match inter i1 i2 with
| None -> None (* Could directly raise a system contradiction exception *)
| Some bnd ->
- Some { pos = p1 ; neg = n1 ; bound = bnd ; prf = And(prf1,prf2) }
+ Some { pos = p1 ; neg = n1 ; bound = bnd ; prf = And(prf1,prf2) }
(** [xadd_cstr vect cstr_info] loads an constraint into the system.
The constraint is neither redundant nor contradictory.
@@ -107,14 +107,14 @@ let xadd_cstr vect cstr_info sys =
try
let info = System.find sys vect in
match merge_cstr_info cstr_info !info with
- | None -> raise (SystemContradiction (And(cstr_info.prf, (!info).prf)))
- | Some info' -> info := info'
+ | None -> raise (SystemContradiction (And(cstr_info.prf, (!info).prf)))
+ | Some info' -> info := info'
with
- | Not_found -> System.replace sys vect (ref cstr_info)
+ | Not_found -> System.replace sys vect (ref cstr_info)
exception TimeOut
-
-let xadd_cstr vect cstr_info sys =
+
+let xadd_cstr vect cstr_info sys =
if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ;
if System.length sys < !max_nb_cstr
then xadd_cstr vect cstr_info sys
@@ -122,11 +122,11 @@ let xadd_cstr vect cstr_info sys =
type cstr_ext =
| Contradiction (** The constraint is contradictory.
- Typically, a [SystemContradiction] exception will be raised. *)
+ Typically, a [SystemContradiction] exception will be raised. *)
| Redundant (** The constrain is redundant.
- Typically, the constraint will be dropped *)
+ Typically, the constraint will be dropped *)
| Cstr of vector * cstr_info (** Taken alone, the constraint is neither contradictory nor redundant.
- Typically, it will be added to the constraint system. *)
+ Typically, it will be added to the constraint system. *)
(** [normalise_cstr] : vector -> cstr_info -> cstr_ext *)
let normalise_cstr vect cinfo =
@@ -136,8 +136,8 @@ let normalise_cstr vect cinfo =
match Vect.choose vect with
| None -> if Itv.in_bound (l,r) (Int 0) then Redundant else Contradiction
| Some (_,n,_) -> Cstr(Vect.div n vect,
- let divn x = x // n in
- if Int.equal (sign_num n) 1
+ let divn x = x // n in
+ if Int.equal (sign_num n) 1
then{cinfo with bound = (Option.map divn l , Option.map divn r) }
else {cinfo with pos = cinfo.neg ; neg = cinfo.pos ; bound = (Option.map divn r , Option.map divn l)})
@@ -157,11 +157,11 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
normalise_cstr v {pos = p ; neg = n ; bound =
(match o with
- | Eq -> Some c , Some c
+ | Eq -> Some c , Some c
| Ge -> Some c , None
| Gt -> raise Polynomial.Strict
) ;
- prf = Assum idx }
+ prf = Assum idx }
(** [load_system l] takes a list of constraints of type [cstr_compat]
@@ -179,7 +179,7 @@ let load_system l =
| Contradiction -> raise (SystemContradiction (Assum i))
| Redundant -> vrs
| Cstr(vect,info) ->
- xadd_cstr vect info sys ;
+ xadd_cstr vect info sys ;
Vect.fold (fun s v _ -> ISet.add v s) vrs cstr.coeffs) ISet.empty li in
{sys = sys ;vars = vars}
@@ -218,7 +218,7 @@ let add (v1,c1) (v2,c2) =
let split x (vect: vector) info (l,m,r) =
match get x vect with
| Int 0 -> (* The constraint does not mention [x], store it in m *)
- (l,(vect,info)::m,r)
+ (l,(vect,info)::m,r)
| vl -> (* otherwise *)
let cons_bound lst bd =
@@ -257,10 +257,10 @@ let project vr sys =
List.iter(fun l_elem -> List.iter (fun r_elem ->
let (vect,info) = elim l_elem r_elem in
- match normalise_cstr vect info with
- | Redundant -> ()
- | Contradiction -> raise (SystemContradiction info.prf)
- | Cstr(vect,info) -> xadd_cstr vect info new_sys) r ) l;
+ match normalise_cstr vect info with
+ | Redundant -> ()
+ | Contradiction -> raise (SystemContradiction info.prf)
+ | Cstr(vect,info) -> xadd_cstr vect info new_sys) r ) l;
{sys = new_sys ; vars = ISet.remove vr sys.vars}
@@ -277,20 +277,20 @@ let project_using_eq vr c vect bound prf (vect',info') =
match get vr vect' with
| Int 0 -> (vect',info')
| c2 ->
- let c1 = if c2 >=/ Int 0 then minus_num c else c in
+ let c1 = if c2 >=/ Int 0 then minus_num c else c in
- let c2 = abs_num c2 in
+ let c2 = abs_num c2 in
- let (vres,(n,p)) = add (vect,c1) (vect', c2) in
+ let (vres,(n,p)) = add (vect,c1) (vect', c2) in
- let cst = bound // c1 in
+ let cst = bound // c1 in
- let bndres =
- let f x = cst +/ x // c2 in
- let (l,r) = info'.bound in
+ let bndres =
+ let f x = cst +/ x // c2 in
+ let (l,r) = info'.bound in
(Option.map f l , Option.map f r) in
- (vres,{neg = n ; pos = p ; bound = bndres ; prf = Elim(vr,prf,info'.prf)})
+ (vres,{neg = n ; pos = p ; bound = bndres ; prf = Elim(vr,prf,info'.prf)})
let elim_var_using_eq vr vect cst prf sys =
@@ -302,10 +302,10 @@ let elim_var_using_eq vr vect cst prf sys =
System.iter(fun vect iref ->
let (vect',info') = elim_var (vect,!iref) in
- match normalise_cstr vect' info' with
- | Redundant -> ()
- | Contradiction -> raise (SystemContradiction info'.prf)
- | Cstr(vect,info') -> xadd_cstr vect info' new_sys) sys.sys ;
+ match normalise_cstr vect' info' with
+ | Redundant -> ()
+ | Contradiction -> raise (SystemContradiction info'.prf)
+ | Cstr(vect,info') -> xadd_cstr vect info' new_sys) sys.sys ;
{sys = new_sys ; vars = ISet.remove vr sys.vars}
@@ -337,8 +337,8 @@ let restrict_bound n sum (itv:interval) =
let l,r = itv in
match sign_num n with
| 0 -> if in_bound itv sum
- then (None,None) (* redundant *)
- else failwith "SystemContradiction"
+ then (None,None) (* redundant *)
+ else failwith "SystemContradiction"
| 1 -> Option.map f l , Option.map f r
| _ -> Option.map f r , Option.map f l
@@ -355,7 +355,7 @@ let bound_of_variable map v sys =
Vect.pp vect (Num.string_of_num sum) Vect.pp rst ;
Printf.fprintf stdout "current interval: %a\n" Itv.pp (!iref).bound;
failwith "bound_of_variable: impossible"
- | Some itv -> itv) sys (None,None)
+ | Some itv -> itv) sys (None,None)
(** [pick_small_value bnd] picks a value being closed to zero within the interval *)
@@ -365,10 +365,10 @@ let pick_small_value bnd =
| None , Some i -> if (Int 0) <=/ (floor_num i) then Int 0 else floor_num i
| Some i,None -> if i <=/ (Int 0) then Int 0 else ceiling_num i
| Some i,Some j ->
- if i <=/ Int 0 && Int 0 <=/ j
- then Int 0
- else if ceiling_num i <=/ floor_num j
- then ceiling_num i (* why not *) else i
+ if i <=/ Int 0 && Int 0 <=/ j
+ then Int 0
+ else if ceiling_num i <=/ floor_num j
+ then ceiling_num i (* why not *) else i
(** [solution s1 sys_l = Some(sn,\[(vn-1,sn-1);...; (v1,s1)\]\@sys_l)]
@@ -385,20 +385,20 @@ let solve_sys black_v choose_eq choose_variable sys sys_l =
let eqs = choose_eq sys in
try
- let (v,vect,cst,ln) = fst (List.find (fun ((v,_,_,_),_) -> v <> black_v) eqs) in
- if debug then
+ let (v,vect,cst,ln) = fst (List.find (fun ((v,_,_,_),_) -> v <> black_v) eqs) in
+ if debug then
(Printf.printf "\nE %a = %s variable %i\n" Vect.pp vect (string_of_num cst) v ;
- flush stdout);
- let sys' = elim_var_using_eq v vect cst ln sys in
- solve_sys sys' ((v,sys)::sys_l)
+ flush stdout);
+ let sys' = elim_var_using_eq v vect cst ln sys in
+ solve_sys sys' ((v,sys)::sys_l)
with Not_found ->
let vars = choose_variable sys in
- try
- let (v,est) = (List.find (fun (v,_) -> v <> black_v) vars) in
- if debug then (Printf.printf "\nV : %i estimate %f\n" v est ; flush stdout) ;
- let sys' = project v sys in
- solve_sys sys' ((v,sys)::sys_l)
- with Not_found -> (* we are done *) Inl (sys,sys_l) in
+ try
+ let (v,est) = (List.find (fun (v,_) -> v <> black_v) vars) in
+ if debug then (Printf.printf "\nV : %i estimate %f\n" v est ; flush stdout) ;
+ let sys' = project v sys in
+ solve_sys sys' ((v,sys)::sys_l)
+ with Not_found -> (* we are done *) Inl (sys,sys_l) in
solve_sys sys sys_l
@@ -408,7 +408,7 @@ let solve black_v choose_eq choose_variable cstrs =
try
let sys = load_system cstrs in
- if debug then Printf.printf "solve :\n %a" pp_system sys.sys ;
+ if debug then Printf.printf "solve :\n %a" pp_system sys.sys ;
solve_sys black_v choose_eq choose_variable sys []
with SystemContradiction prf -> Inr prf
@@ -430,20 +430,20 @@ struct
match Vect.choose l1 with
| None -> xpart rl ((Vect.null,info)::ltl) n (info.neg+info.pos+z) p
| Some(vr, vl, rl1) ->
- if Int.equal v vr
- then
- let cons_bound lst bd =
- match bd with
- | None -> lst
- | Some bnd -> info.neg+info.pos::lst in
-
- let lb,rb = info.bound in
- if Int.equal (sign_num vl) 1
- then xpart rl ((rl1,info)::ltl) (cons_bound n lb) z (cons_bound p rb)
- else xpart rl ((rl1,info)::ltl) (cons_bound n rb) z (cons_bound p lb)
- else
- (* the variable is greater *)
- xpart rl ((l1,info)::ltl) n (info.neg+info.pos+z) p
+ if Int.equal v vr
+ then
+ let cons_bound lst bd =
+ match bd with
+ | None -> lst
+ | Some bnd -> info.neg+info.pos::lst in
+
+ let lb,rb = info.bound in
+ if Int.equal (sign_num vl) 1
+ then xpart rl ((rl1,info)::ltl) (cons_bound n lb) z (cons_bound p rb)
+ else xpart rl ((rl1,info)::ltl) (cons_bound n rb) z (cons_bound p lb)
+ else
+ (* the variable is greater *)
+ xpart rl ((l1,info)::ltl) n (info.neg+info.pos+z) p
in
let (sys',n,z,p) = xpart l [] [] 0 [] in
@@ -484,15 +484,15 @@ struct
match Vect.choose l with
| None -> (false,Vect.null)
| Some(i,_,rl) -> if Int.equal i v
- then (true,rl)
- else if i < v then unroll_until v rl else (false,l)
+ then (true,rl)
+ else if i < v then unroll_until v rl else (false,l)
- let rec choose_simple_equation eqs =
+ let rec choose_simple_equation eqs =
match eqs with
| [] -> None
- | (vect,a,prf,ln)::eqs ->
+ | (vect,a,prf,ln)::eqs ->
match Vect.choose vect with
| Some(i,v,rst) -> if Vect.is_null rst
then Some (i,vect,a,prf,ln)
@@ -507,29 +507,29 @@ struct
*)
let is_primal_equation_var v =
List.fold_left (fun nb_eq (vect,info) ->
- if fst (unroll_until v vect)
- then if itv_point info.bound then nb_eq + 1 else nb_eq
- else nb_eq) 0 sys_l in
+ if fst (unroll_until v vect)
+ then if itv_point info.bound then nb_eq + 1 else nb_eq
+ else nb_eq) 0 sys_l in
let rec find_var vect =
match Vect.choose vect with
| None -> None
| Some(i,_,vect) ->
- let nb_eq = is_primal_equation_var i in
- if Int.equal nb_eq 2
- then Some i else find_var vect in
+ let nb_eq = is_primal_equation_var i in
+ if Int.equal nb_eq 2
+ then Some i else find_var vect in
let rec find_eq_var eqs =
match eqs with
- | [] -> None
- | (vect,a,prf,ln)::l ->
- match find_var vect with
- | None -> find_eq_var l
- | Some r -> Some (r,vect,a,prf,ln)
+ | [] -> None
+ | (vect,a,prf,ln)::l ->
+ match find_var vect with
+ | None -> find_eq_var l
+ | Some r -> Some (r,vect,a,prf,ln)
in
match choose_simple_equation eqs with
- | None -> find_eq_var eqs
- | Some res -> Some res
+ | None -> find_eq_var eqs
+ | Some res -> Some res
@@ -539,43 +539,43 @@ struct
let equalities = List.fold_left
(fun l (vect,info) ->
- match info.bound with
- | Some a , Some b ->
- if a =/ b then (* This an equation *)
- (vect,a,info.prf,info.neg+info.pos)::l else l
- | _ -> l
+ match info.bound with
+ | Some a , Some b ->
+ if a =/ b then (* This an equation *)
+ (vect,a,info.prf,info.neg+info.pos)::l else l
+ | _ -> l
) [] sys_l in
let rec estimate_cost v ct sysl acc tlsys =
match sysl with
- | [] -> (acc,tlsys)
- | (l,info)::rsys ->
- let ln = info.pos + info.neg in
- let (b,l) = unroll_until v l in
- match b with
- | true ->
- if itv_point info.bound
- then estimate_cost v ct rsys (acc+ln) ((l,info)::tlsys) (* this is free *)
- else estimate_cost v ct rsys (acc+ln+ct) ((l,info)::tlsys) (* should be more ? *)
- | false -> estimate_cost v ct rsys (acc+ln) ((l,info)::tlsys) in
+ | [] -> (acc,tlsys)
+ | (l,info)::rsys ->
+ let ln = info.pos + info.neg in
+ let (b,l) = unroll_until v l in
+ match b with
+ | true ->
+ if itv_point info.bound
+ then estimate_cost v ct rsys (acc+ln) ((l,info)::tlsys) (* this is free *)
+ else estimate_cost v ct rsys (acc+ln+ct) ((l,info)::tlsys) (* should be more ? *)
+ | false -> estimate_cost v ct rsys (acc+ln) ((l,info)::tlsys) in
match choose_primal_equation equalities sys_l with
- | None ->
- let cost_eq eq const prf ln acc_costs =
+ | None ->
+ let cost_eq eq const prf ln acc_costs =
- let rec cost_eq eqr sysl costs =
+ let rec cost_eq eqr sysl costs =
match Vect.choose eqr with
| None -> costs
| Some(v,_,eqr) -> let (cst,tlsys) = estimate_cost v (ln-1) sysl 0 [] in
- cost_eq eqr tlsys (((v,eq,const,prf),cst)::costs) in
- cost_eq eq sys_l acc_costs in
+ cost_eq eqr tlsys (((v,eq,const,prf),cst)::costs) in
+ cost_eq eq sys_l acc_costs in
- let all_costs = List.fold_left (fun all_costs (vect,const,prf,ln) -> cost_eq vect const prf ln all_costs) [] equalities in
+ let all_costs = List.fold_left (fun all_costs (vect,const,prf,ln) -> cost_eq vect const prf ln all_costs) [] equalities in
- (* pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
+ (* pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
- List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs
- | Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]
+ List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs
+ | Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]
end
@@ -593,12 +593,12 @@ struct
op = Eq ;
cst = (Int 0)} in
match solve fresh choose_equality_var choose_variable (cstr::l) with
- | Inr prf -> None (* This is an unsatisfiability proof *)
- | Inl (s,_) ->
- try
- Some (bound_of_variable IMap.empty fresh s.sys)
- with x when CErrors.noncritical x ->
- Printf.printf "optimise Exception : %s" (Printexc.to_string x);
+ | Inr prf -> None (* This is an unsatisfiability proof *)
+ | Inl (s,_) ->
+ try
+ Some (bound_of_variable IMap.empty fresh s.sys)
+ with x when CErrors.noncritical x ->
+ Printf.printf "optimise Exception : %s" (Printexc.to_string x);
None
@@ -608,16 +608,16 @@ struct
| Inr prf -> Inr prf
| Inl (_,l) ->
- let rec rebuild_solution l map =
- match l with
- | [] -> map
- | (v,e)::l ->
- let itv = bound_of_variable map v e.sys in
- let map = IMap.add v (pick_small_value itv) map in
- rebuild_solution l map
- in
+ let rec rebuild_solution l map =
+ match l with
+ | [] -> map
+ | (v,e)::l ->
+ let itv = bound_of_variable map v e.sys in
+ let map = IMap.add v (pick_small_value itv) map in
+ rebuild_solution l map
+ in
- let map = rebuild_solution l IMap.empty in
+ let map = rebuild_solution l IMap.empty in
let vect = IMap.fold (fun v i vect -> Vect.set v i vect) map Vect.null in
if debug then Printf.printf "SOLUTION %a" Vect.pp vect ;
let res = Inl vect in
@@ -645,9 +645,9 @@ struct
let forall_pairs f l1 l2 =
List.fold_left (fun acc e1 ->
List.fold_left (fun acc e2 ->
- match f e1 e2 with
- | None -> acc
- | Some v -> v::acc) acc l2) [] l1
+ match f e1 e2 with
+ | None -> acc
+ | Some v -> v::acc) acc l2) [] l1
let add_op x y =
@@ -664,8 +664,8 @@ struct
| Int 0 , _ | _ , Int 0 -> None
| a , b ->
if Int.equal ((sign_num a) * (sign_num b)) (-1)
- then
- Some (add (p1,abs_num a) (p2,abs_num b) ,
+ then
+ Some (add (p1,abs_num a) (p2,abs_num b) ,
{coeffs = add (v1,abs_num a) (v2,abs_num b) ;
op = add_op op1 op2 ;
cst = n1 // (abs_num a) +/ n2 // (abs_num b) })
@@ -675,12 +675,12 @@ struct
op = add_op op1 op2;
cst = n1 // (minus_num (a// b)) +/ n2 // (Int 1)})
else if op2 == Eq
- then
- Some (add (p2,minus_num (b // a)) (p1,Int 1),
+ then
+ Some (add (p2,minus_num (b // a)) (p1,Int 1),
{coeffs = add (v2,minus_num (b// a)) (v1 ,Int 1) ;
op = add_op op1 op2;
cst = n2 // (minus_num (b// a)) +/ n1 // (Int 1)})
- else None (* op2 could be Eq ... this might happen *)
+ else None (* op2 could be Eq ... this might happen *)
let normalise_proofs l =
@@ -752,10 +752,10 @@ let mk_proof hyps prf =
match prfs with
| Inr x -> [x]
| Inl (oleft,oright) ->
- match oleft , oright with
- | None , None -> []
- | None , Some(prf,cstr,_) | Some(prf,cstr,_) , None -> [prf,cstr]
- | Some(prf1,cstr1,_) , Some(prf2,cstr2,_) -> [prf1,cstr1;prf2,cstr2] in
+ match oleft , oright with
+ | None , None -> []
+ | None , Some(prf,cstr,_) | Some(prf,cstr,_) , None -> [prf,cstr]
+ | Some(prf1,cstr1,_) , Some(prf2,cstr2,_) -> [prf1,cstr1;prf2,cstr2] in
mk_proof prf
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index cca66c0719..a30e963f2a 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -66,7 +66,7 @@ let rec try_any l x =
let all_pairs f l =
let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
- let rec xpairs acc l =
+ let rec xpairs acc l =
match l with
| [] -> acc
| e::lx -> xpairs (pair_with acc e l) lx in
@@ -77,20 +77,20 @@ let rec is_sublist f l1 l2 =
| [] ,_ -> true
| e::l1', [] -> false
| e::l1' , e'::l2' ->
- if f e e' then is_sublist f l1' l2'
- else is_sublist f l1 l2'
-
-let extract pred l =
- List.fold_left (fun (fd,sys) e ->
- match fd with
- | None ->
- begin
- match pred e with
- | None -> fd, e::sys
- | Some v -> Some(v,e) , sys
- end
- | _ -> (fd, e::sys)
- ) (None,[]) l
+ if f e e' then is_sublist f l1' l2'
+ else is_sublist f l1 l2'
+
+let extract pred l =
+ List.fold_left (fun (fd,sys) e ->
+ match fd with
+ | None ->
+ begin
+ match pred e with
+ | None -> fd, e::sys
+ | Some v -> Some(v,e) , sys
+ end
+ | _ -> (fd, e::sys)
+ ) (None,[]) l
let extract_best red lt l =
let rec extractb c e rst l =
@@ -338,7 +338,7 @@ struct
end
(**
- * MODULE: Labels for atoms in propositional formulas.
+ * MODULE: Labels for atoms in propositional formulas.
* Tags are used to identify unused atoms in CNFs, and propagate them back to
* the original formula. The translation back to Coq then ignores these
* superfluous items, which speeds the translation up a bit.
@@ -406,26 +406,26 @@ let command exe_path args vl =
finally
(* Recover the result *)
- (fun () ->
- match status with
- | Unix.WEXITED 0 ->
- let inch = Unix.in_channel_of_descr stdout_read in
- begin
+ (fun () ->
+ match status with
+ | Unix.WEXITED 0 ->
+ let inch = Unix.in_channel_of_descr stdout_read in
+ begin
try Marshal.from_channel inch
with any ->
failwith
(Printf.sprintf "command \"%s\" exited %s" exe_path
(Printexc.to_string any))
end
- | Unix.WEXITED i ->
+ | Unix.WEXITED i ->
failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
- | Unix.WSIGNALED i ->
+ | Unix.WSIGNALED i ->
failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
- | Unix.WSTOPPED i ->
+ | Unix.WSTOPPED i ->
failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
(* Cleanup *)
- (fun () ->
- List.iter (fun x -> try Unix.close x with any -> ())
+ (fun () ->
+ List.iter (fun x -> try Unix.close x with any -> ())
[stdin_read; stdin_write;
stdout_read; stdout_write;
stderr_read; stderr_write])
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 14e2e40846..28d8d5a020 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -49,9 +49,9 @@ struct
type 'a t =
{
- outch : out_channel ;
- mutable status : mode ;
- htbl : 'a Table.t
+ outch : out_channel ;
+ mutable status : mode ;
+ htbl : 'a Table.t
}
@@ -72,49 +72,49 @@ let read_key_elem inch =
| End_of_file -> None
| e when CErrors.noncritical e -> raise InvalidTableFormat
-(**
+(**
We used to only lock/unlock regions.
- Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]?
+ Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]?
In case of locking failure, the cache is not used.
**)
type lock_kind = Read | Write
-let lock kd fd =
- let pos = lseek fd 0 SEEK_CUR in
- let success =
- try
+let lock kd fd =
+ let pos = lseek fd 0 SEEK_CUR in
+ let success =
+ try
ignore (lseek fd 0 SEEK_SET);
- let lk = match kd with
- | Read -> F_RLOCK
- | Write -> F_LOCK in
+ let lk = match kd with
+ | Read -> F_RLOCK
+ | Write -> F_LOCK in
lockf fd lk 1; true
with Unix.Unix_error(_,_,_) -> false in
- ignore (lseek fd pos SEEK_SET) ;
+ ignore (lseek fd pos SEEK_SET) ;
success
-let unlock fd =
+let unlock fd =
let pos = lseek fd 0 SEEK_CUR in
- try
- ignore (lseek fd 0 SEEK_SET) ;
+ try
+ ignore (lseek fd 0 SEEK_SET) ;
lockf fd F_ULOCK 1
- with
- Unix.Unix_error(_,_,_) -> ()
- (* Here, this is really bad news --
+ with
+ Unix.Unix_error(_,_,_) -> ()
+ (* Here, this is really bad news --
there is a pending lock which could cause a deadlock.
Should it be an anomaly or produce a warning ?
*);
- ignore (lseek fd pos SEEK_SET)
+ ignore (lseek fd pos SEEK_SET)
(* We make the assumption that an acquired lock can always be released *)
-let do_under_lock kd fd f =
+let do_under_lock kd fd f =
if lock kd fd
then
finally f (fun () -> unlock fd)
else f ()
-
+
let open_in f =
@@ -128,11 +128,11 @@ let open_in f =
| None -> ()
| Some (key,elem) ->
Table.add htbl key elem ;
- xload () in
+ xload () in
try
(* Locking of the (whole) file while reading *)
- do_under_lock Read finch xload ;
- close_in_noerr inch ;
+ do_under_lock Read finch xload ;
+ close_in_noerr inch ;
{
outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ;
status = Open ;
@@ -145,11 +145,11 @@ let open_in f =
let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
let out = (openfile f flags 0o666) in
let outch = out_channel_of_descr out in
- do_under_lock Write out
- (fun () ->
- Table.iter
- (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
- flush outch) ;
+ do_under_lock Write out
+ (fun () ->
+ Table.iter
+ (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
+ flush outch) ;
{ outch = outch ;
status = Open ;
htbl = htbl
@@ -165,8 +165,8 @@ let add t k e =
let fd = descr_of_out_channel outch in
begin
Table.add tbl k e ;
- do_under_lock Write fd
- (fun _ ->
+ do_under_lock Write fd
+ (fun _ ->
Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
flush outch
)
@@ -178,7 +178,7 @@ let find t k =
then raise UnboundTable
else
let res = Table.find tbl k in
- res
+ res
let memo cache f =
let tbl = lazy (try Some (open_in cache) with _ -> None) in
@@ -186,13 +186,13 @@ let memo cache f =
match Lazy.force tbl with
| None -> f x
| Some tbl ->
- try
- find tbl x
- with
- Not_found ->
- let res = f x in
- add tbl x res ;
- res
+ try
+ find tbl x
+ with
+ Not_found ->
+ let res = f x in
+ add tbl x res ;
+ res
let memo_cond cache cond f =
let tbl = lazy (try Some (open_in cache) with _ -> None) in
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index 58d5d7ecf1..0a0ffc7947 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -525,11 +525,11 @@ let deepen_until limit f n =
| 0 -> raise TooDeep
| -1 -> deepen f n
| _ ->
- let rec d_until f n =
- try(* if !debugging
- then (print_string "Searching with depth limit ";
- print_int n; print_newline()) ;*) f n
- with Failure x ->
- (*if !debugging then (Printf.printf "solver error : %s\n" x) ; *)
- if n = limit then raise TooDeep else d_until f (n + 1) in
- d_until f n
+ let rec d_until f n =
+ try(* if !debugging
+ then (print_string "Searching with depth limit ";
+ print_int n; print_newline()) ;*) f n
+ with Failure x ->
+ (*if !debugging then (Printf.printf "solver error : %s\n" x) ; *)
+ if n = limit then raise TooDeep else d_until f (n + 1) in
+ d_until f n
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 17:16:54 +0000