From c1af34823c62ce7eced1c4d8a695384ef789d3b1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 17 Mar 2015 17:33:35 +0100 Subject: [PATCH] Fix for compilation on older ocaml compiler --- solver/mcproof.ml | 12 ++++++++++-- solver/mcproof.mli | 6 ++++-- solver/mcsolver_types.mli | 8 +++++--- solver/res.ml | 12 ++++++++++-- solver/res.mli | 6 ++++-- solver/solver_types.mli | 6 ++++-- 6 files changed, 37 insertions(+), 13 deletions(-) diff --git a/solver/mcproof.ml b/solver/mcproof.ml index a44f0601..10cd3380 100644 --- a/solver/mcproof.ml +++ b/solver/mcproof.ml @@ -71,13 +71,21 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct let resolved, new_clause = aux [] [] l in resolved, List.rev new_clause + (* List.sort_uniq is only since 4.02.0 *) + let sort_uniq compare l = + let rec aux = function + | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r + | l -> l + in + aux (List.sort compare l) + let to_list c = let v = St.(c.atoms) in let l = ref [] in for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - let res = List.sort_uniq compare_atoms !l in + let res = sort_uniq compare_atoms !l in let l, _ = resolve res in if l <> [] then L.debug 3 "Input clause is a tautology"; @@ -251,7 +259,7 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct | Resolution (proof1, proof2, _) -> aux (aux acc proof1) proof2 in - List.sort_uniq compare_cl (aux [] proof) + sort_uniq compare_cl (aux [] proof) (* Print proof graph *) let _i = ref 0 diff --git a/solver/mcproof.mli b/solver/mcproof.mli index d80cba71..cb7b2167 100644 --- a/solver/mcproof.mli +++ b/solver/mcproof.mli @@ -6,6 +6,8 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (L : Log_intf.S)(St : Mcsolver_types.S) - -> S with type atom = St.atom and type clause = St.clause and type lemma = St.proof +module Make : + functor (L : Log_intf.S) -> + functor (St : Mcsolver_types.S) -> + S with type atom = St.atom and type clause = St.clause and type lemma = St.proof (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/mcsolver_types.mli b/solver/mcsolver_types.mli index 85276113..a10ae5f5 100644 --- a/solver/mcsolver_types.mli +++ b/solver/mcsolver_types.mli @@ -13,7 +13,9 @@ module type S = Mcsolver_types_intf.S -module Make : functor (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with - type term = E.Term.t and type formula = E.Formula.t) - -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof +module Make : + functor (L : Log_intf.S) -> + functor (E : Expr_intf.S) -> + functor (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) -> + S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *) diff --git a/solver/res.ml b/solver/res.ml index a068ba1a..f8615def 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -71,13 +71,21 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct let resolved, new_clause = aux [] [] l in resolved, List.rev new_clause + (* List.sort_uniq is only since 4.02.0 *) + let sort_uniq compare l = + let rec aux = function + | x :: ((y :: _) as r) -> if compare x y = 0 then aux r else x :: aux r + | l -> l + in + aux (List.sort compare l) + let to_list c = let v = St.(c.atoms) in let l = ref [] in for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - let l, res = resolve (List.sort_uniq compare_atoms !l) in + let l, res = resolve (sort_uniq compare_atoms !l) in if l <> [] then raise (Resolution_error "Input clause is a tautology"); res @@ -250,7 +258,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct | Resolution (proof1, proof2, _) -> aux (aux acc proof1) proof2 in - List.sort_uniq compare_cl (aux [] proof) + sort_uniq compare_cl (aux [] proof) (* Print proof graph *) let _i = ref 0 diff --git a/solver/res.mli b/solver/res.mli index 33a44da8..306a724d 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -6,6 +6,8 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S -module Make : functor (L : Log_intf.S)(St : Solver_types.S) - -> S with type atom= St.atom and type clause = St.clause and type lemma = St.proof +module Make : + functor (L : Log_intf.S) -> + functor (St : Solver_types.S) -> + S with type atom= St.atom and type clause = St.clause and type lemma = St.proof (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/solver_types.mli b/solver/solver_types.mli index ecc41d8b..d4fa2200 100644 --- a/solver/solver_types.mli +++ b/solver/solver_types.mli @@ -13,6 +13,8 @@ module type S = Solver_types_intf.S -module Make : functor (F : Formula_intf.S)(Th : Theory_intf.S) - -> S with type formula = F.t and type proof = Th.proof +module Make : + functor (F : Formula_intf.S) -> + functor (Th : Theory_intf.S) -> + S with type formula = F.t and type proof = Th.proof (** Functor to instantiate the types of clauses for the Solver. *)