From eb692230d334bbc1f8c4b32fb335098635add700 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 29 Oct 2014 18:51:32 +0100 Subject: [PATCH] Begun Functoring the sat solver. New folder to distinguish sat solver from smt solver. --- {smt => sat}/.merlin | 0 sat/explanation.ml | 70 +++++++++++++++++++++++++++++++ {smt => sat}/explanation.mli | 24 +---------- sat/explanation_intf.ml | 35 ++++++++++++++++ sat/formula_intf.ml | 40 ++++++++++++++++++ {smt => sat}/solver.ml | 27 ++++++------ {smt => sat}/solver.mli | 23 +++++----- {smt => sat}/solver_types.ml | 69 ++++-------------------------- sat/solver_types.mli | 16 +++++++ sat/solver_types_intf.ml | 79 +++++++++++++++++++++++++++++++++++ sat/theory_intf.ml | 27 ++++++++++++ smt/explanation.ml | 69 ------------------------------ smt/solver_types.mli | 81 ------------------------------------ 13 files changed, 303 insertions(+), 257 deletions(-) rename {smt => sat}/.merlin (100%) create mode 100644 sat/explanation.ml rename {smt => sat}/explanation.mli (71%) create mode 100644 sat/explanation_intf.ml create mode 100644 sat/formula_intf.ml rename {smt => sat}/solver.ml (98%) rename {smt => sat}/solver.mli (69%) rename {smt => sat}/solver_types.ml (74%) create mode 100644 sat/solver_types.mli create mode 100644 sat/solver_types_intf.ml create mode 100644 sat/theory_intf.ml delete mode 100644 smt/explanation.ml delete mode 100644 smt/solver_types.mli diff --git a/smt/.merlin b/sat/.merlin similarity index 100% rename from smt/.merlin rename to sat/.merlin diff --git a/sat/explanation.ml b/sat/explanation.ml new file mode 100644 index 00000000..380f8ef0 --- /dev/null +++ b/sat/explanation.ml @@ -0,0 +1,70 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Format + +module Make(Stypes : Solver_types.S) = struct + + type atom = Stypes.atom + + type exp = Atom of atom | Fresh of int + + module S = Set.Make(struct + type t = exp + let compare a b = match a,b with + | Atom _, Fresh _ -> -1 + | Fresh _, Atom _ -> 1 + | Fresh i1, Fresh i2 -> i1 - i2 + | Atom a, Atom b -> a.aid - b.aid + end) + + type t = S.t + + let singleton e = S.singleton (Atom e) + + let empty = S.empty + + let union s1 s2 = S.union s1 s2 + + let iter_atoms f s = + S.iter (fun e -> match e with + | Fresh _ -> () + | Atom a -> f a) s + + let fold_atoms f s acc = + S.fold (fun e acc -> match e with + | Fresh _ -> acc + | Atom a -> f a acc) s acc + + let merge e1 e2 = e1 + + let fresh_exp = + let r = ref (-1) in + fun () -> incr r; !r + + let remove_fresh i s = + let fi = Fresh i in + if S.mem fi s then Some (S.remove fi s) + else None + + let add_fresh i = S.add (Fresh i) + + let print fmt ex = + fprintf fmt "{"; + S.iter (function + | Atom a -> fprintf fmt "%a, " Stypes.pp_atom a + | Fresh i -> fprintf fmt "Fresh%d " i) ex; + fprintf fmt "}" + +end diff --git a/smt/explanation.mli b/sat/explanation.mli similarity index 71% rename from smt/explanation.mli rename to sat/explanation.mli index 5a0e0db9..f6675ee6 100644 --- a/smt/explanation.mli +++ b/sat/explanation.mli @@ -12,26 +12,6 @@ (* *) (**************************************************************************) -type t +module type S = Explanation_intf.S -type exp - -val empty : t - -val singleton : Solver_types.atom -> t - -val union : t -> t -> t - -val merge : t -> t -> t - -val iter_atoms : (Solver_types.atom -> unit) -> t -> unit - -val fold_atoms : (Solver_types.atom -> 'a -> 'a ) -> t -> 'a -> 'a - -val fresh_exp : unit -> int - -val remove_fresh : int -> t -> t option - -val add_fresh : int -> t -> t - -val print : Format.formatter -> t -> unit +module Make : functor (St : Solver_types.S) -> S with type atom = St.atom diff --git a/sat/explanation_intf.ml b/sat/explanation_intf.ml new file mode 100644 index 00000000..1e3e5fc0 --- /dev/null +++ b/sat/explanation_intf.ml @@ -0,0 +1,35 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + + type t + type exp + type atom + + val empty : t + val singleton : atom -> t + + val union : t -> t -> t + val merge : t -> t -> t + + val iter_atoms : (atom -> unit) -> t -> unit + val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a + + val fresh_exp : unit -> int + val add_fresh : int -> t -> t + val remove_fresh : int -> t -> t option + + val print : Format.formatter -> t -> unit +end diff --git a/sat/formula_intf.ml b/sat/formula_intf.ml new file mode 100644 index 00000000..60ce4037 --- /dev/null +++ b/sat/formula_intf.ml @@ -0,0 +1,40 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Guillaume Bury *) +(* INRIA *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + + type t + + val vrai : t + val faux : t + val dummy : t + + val neg : t -> t + val norm : t -> t * bool + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + + val label : t -> Hstring.t + val add_label : Hstring.t -> t -> unit + + val print : Format.formatter -> t -> unit + + module Map : Map.S with type key = t + module Set : Set.S with type elt = t + +end + diff --git a/smt/solver.ml b/sat/solver.ml similarity index 98% rename from smt/solver.ml rename to sat/solver.ml index 51b6fecc..b1e0b45c 100644 --- a/smt/solver.ml +++ b/sat/solver.ml @@ -10,11 +10,14 @@ (* *) (**************************************************************************) -open Solver_types open Format -module Th = Cc.Make(Combine.CX) -module Ex = Explanation +module Make(F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) = struct + +module Stypes = Solver_types.Make(F) +module Ex = Explanation.Make(Stypes) + +open Stypes exception Sat exception Unsat of clause list @@ -130,17 +133,12 @@ type env = exception Conflict of clause -module Make (Dummy : sig end) = struct - - module Solver_types = Solver_types.Make(struct end) - - open Solver_types type state = { env : env; st_cpt_mk_var: int; - st_ma : var Literal.LT.Map.t; + st_ma : var F.Map.t; } @@ -413,7 +411,7 @@ let expensive_theory_propagate () = None (* ignore(Th.expensive_processing env.tenv); *) (* if D1.d then eprintf "expensive_theory_propagate => None@."; *) (* None *) - (* with Exception.Inconsistent dep -> *) + (* with Th.Inconsistent dep -> *) (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) (* Some dep *) @@ -436,11 +434,11 @@ let theory_propagate () = let full_model = nb_assigns() = env.nb_init_vars in env.tenv <- List.fold_left - (fun t (a,ex) -> let t,_,_ = Th.assume ~cs:true a ex t in t) + (fun t (a,ex) -> let t = Th.assume ~cs:true a ex t in t) env.tenv !facts; if full_model then expensive_theory_propagate () else None - with Exception.Inconsistent dep -> + with Th.Inconsistent dep -> (* eprintf "th inconsistent : %a @." Ex.print dep; *) Some dep @@ -697,12 +695,12 @@ let check_inconsistence_of dep = let env = ref (Th.empty()) in (); Ex.iter_atoms (fun atom -> - let t,_,_ = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in + let t = Th.assume ~cs:true atom.lit (Ex.singleton atom) !env in env := t) dep; (* ignore (Th.expensive_processing !env); *) assert false - with Exception.Inconsistent _ -> () + with Th.Inconsistent _ -> () let theory_analyze dep = let atoms, sz, max_lvl, c_hist = @@ -1030,4 +1028,5 @@ let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = let var, negated = make_var lit in let truth = var.pa.is_true in if negated then not truth else truth + end diff --git a/smt/solver.mli b/sat/solver.mli similarity index 69% rename from smt/solver.mli rename to sat/solver.mli index 096192eb..7a12ef90 100644 --- a/smt/solver.mli +++ b/sat/solver.mli @@ -11,18 +11,21 @@ (* *) (**************************************************************************) -exception Sat -exception Unsat of Solver_types.clause list +module Make (F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) : sig -module Make (Dummy : sig end) : sig - type state + module St : Solver_types.S with type formula = F.t - val solve : unit -> unit - val assume : Literal.LT.t list list -> cnumber : int -> unit - val clear : unit -> unit + exception Sat + exception Unsat of St.clause list - val eval : Literal.LT.t -> bool - val save : unit -> state - val restore : state -> unit + type state + + val solve : unit -> unit + val assume : F.t list list -> cnumber : int -> unit + val clear : unit -> unit + + val eval : F.t -> bool + val save : unit -> state + val restore : state -> unit end diff --git a/smt/solver_types.ml b/sat/solver_types.ml similarity index 74% rename from smt/solver_types.ml rename to sat/solver_types.ml index 8d1cbf3d..8798c752 100644 --- a/smt/solver_types.ml +++ b/sat/solver_types.ml @@ -21,6 +21,7 @@ let is_le n = Hstring.compare n ale = 0 let is_lt n = Hstring.compare n alt = 0 let is_gt n = Hstring.compare n agt = 0 +module Make (F : Formula_intf.S) = struct type var = { vid : int; @@ -34,7 +35,7 @@ type var = and atom = { var : var; - lit : Literal.LT.t; + lit : F.t; neg : atom; mutable watched : clause Vec.t; mutable is_true : bool; @@ -52,9 +53,7 @@ and reason = clause option and premise = clause list -module Make (Dummy : sig end) = struct - -let dummy_lit = Literal.LT.make (Literal.Eq(Term.vrai,Term.vrai)) +let dummy_lit = F.dummy let rec dummy_var = { vid = -101; @@ -80,8 +79,7 @@ and dummy_clause = learnt = false; cpremise = [] } - -module MA = Literal.LT.Map +module MA = F.Map let ale = Hstring.make "<=" let alt = Hstring.make "<" @@ -90,53 +88,7 @@ let is_le n = Hstring.compare n ale = 0 let is_lt n = Hstring.compare n alt = 0 let is_gt n = Hstring.compare n agt = 0 -let normal_form lit = - match Literal.LT.view lit with - | Literal.Eq (t1,t2) when Term.equal t2 Term.faux -> - Literal.LT.make (Literal.Eq(t1,Term.vrai)), true - - | Literal.Eq (t1,t2) when Term.equal t1 Term.faux -> - Literal.LT.make (Literal.Eq(t2,Term.vrai)), true - - - | Literal.Distinct(false, [t1;t2]) when Term.equal t1 Term.faux -> - Literal.LT.make (Literal.Eq(t2,Term.vrai)), false - - | Literal.Distinct(false, [t1;t2]) when Term.equal t2 Term.faux -> - Literal.LT.make (Literal.Eq(t1,Term.vrai)), false - - | Literal.Distinct(false, [t1;t2]) when Term.equal t1 Term.vrai -> - Literal.LT.make (Literal.Eq(t2,Term.vrai)), true - - | Literal.Distinct(false, [t1;t2]) when Term.equal t2 Term.vrai -> - Literal.LT.make (Literal.Eq(t1,Term.vrai)), true - - | Literal.Distinct(false,[_;_]) -> Literal.LT.neg lit, true - - | Literal.Builtin(true,n,[t1;t2]) when is_gt n -> - Literal.LT.neg lit, true - - | Literal.Builtin(false,n,[t1;t2]) when is_le n -> - Literal.LT.neg lit, true - | _ -> lit, false - - -(* let normal_form lit = *) -(* match Literal.LT.view lit with *) -(* | Literal.Eq (t1,t2) -> *) -(* if Term.equal t2 Term.faux || Term.equal t1 Term.faux then *) -(* Literal.LT.neg lit, true *) -(* else *) -(* lit, false *) - -(* | Literal.Distinct(false,[_;_]) -> Literal.LT.neg lit, true *) -(* | Literal.Builtin(true,n,[t1;t2]) when Builtin.is_gt n -> *) -(* Literal.LT.neg lit, true *) - -(* | Literal.Builtin(false,n,[t1;t2]) when Builtin.is_le n -> *) -(* Literal.LT.neg lit, true *) -(* | _ -> lit, false *) - +let normal_form = F.norm let cpt_mk_var = ref 0 let ma = ref MA.empty @@ -165,7 +117,7 @@ let make_var = aid = cpt_fois_2 (* aid = vid*2 *) } and na = { var = var; - lit = Literal.LT.neg lit; + lit = F.neg lit; watched = Vec.make 10 dummy_clause; neg = pa; is_true = false; @@ -222,10 +174,6 @@ let clear () = cpt_mk_var := 0; ma := MA.empty -end - - - module Debug = struct let sign a = if a==a.var.pa then "" else "-" @@ -253,10 +201,9 @@ module Debug = struct let atom fmt a = fprintf fmt "%s%d%s [lit:%a] vpremise={{%a}}" - (sign a) (a.var.vid+1) (value a) Literal.LT.print a.lit + (sign a) (a.var.vid+1) (value a) F.print a.lit premise a.var.vpremise - let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr @@ -268,6 +215,6 @@ module Debug = struct let clause fmt {name=name; atoms=arr; cpremise=cp} = fprintf fmt "%s:{ %a} cpremise={{%a}}" name atoms_vec arr premise cp - +end end diff --git a/sat/solver_types.mli b/sat/solver_types.mli new file mode 100644 index 00000000..22bf524b --- /dev/null +++ b/sat/solver_types.mli @@ -0,0 +1,16 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = Solver_types_intf.S + +module Make : functor (F : Formula_intf.S) -> S with type formula = F.t diff --git a/sat/solver_types_intf.ml b/sat/solver_types_intf.ml new file mode 100644 index 00000000..a9f25908 --- /dev/null +++ b/sat/solver_types_intf.ml @@ -0,0 +1,79 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + type formula + + type var = { + vid : int; + pa : atom; + na : atom; + mutable weight : float; + mutable seen : bool; + mutable level : int; + mutable reason : reason; + mutable vpremise : premise + } + + and atom = { + var : var; + lit : formula; + neg : atom; + mutable watched : clause Vec.t; + mutable is_true : bool; + aid : int + } + + and clause = { + name : string; + mutable atoms : atom Vec.t; + mutable activity : float; + mutable removed : bool; + learnt : bool; + cpremise : premise + } + + and reason = clause option + + and premise = clause list + + val cpt_mk_var : int ref + module Map : Map.S with type key = formula + val ma : var Map.t ref + + val dummy_var : var + val dummy_atom : atom + val dummy_clause : clause + + val make_var : formula -> var * bool + + val add_atom : formula -> atom + + val make_clause : string -> atom list -> int -> bool -> premise -> clause + + val fresh_name : unit -> string + + val fresh_lname : unit -> string + + val fresh_dname : unit -> string + + val to_float : int -> float + + val to_int : float -> int + val made_vars_info : unit -> int * var list + val clear : unit -> unit + + val pp_atom : Format.formatter -> atom -> unit + val pp_clause : Format.formatter -> clause -> unit +end + diff --git a/sat/theory_intf.ml b/sat/theory_intf.ml new file mode 100644 index 00000000..bf851388 --- /dev/null +++ b/sat/theory_intf.ml @@ -0,0 +1,27 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = sig + type t + type formula + + module St : Solver_types.S with type formula = formula + module Ex : Explanation.S with type atom = St.atom + + exception Inconsistent of Ex.t + + val empty : unit -> t + val assume : cs:bool -> formula -> Ex.t -> t -> t +end + diff --git a/smt/explanation.ml b/smt/explanation.ml deleted file mode 100644 index d14f162a..00000000 --- a/smt/explanation.ml +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Stephane Lescuyer *) -(* INRIA, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -open Solver_types -open Format - -type exp = Atom of Solver_types.atom | Fresh of int - -module S = - Set.Make - (struct - type t = exp - let compare a b = match a,b with - | Atom _, Fresh _ -> -1 - | Fresh _, Atom _ -> 1 - | Fresh i1, Fresh i2 -> i1 - i2 - | Atom a, Atom b -> a.aid - b.aid - end) - -type t = S.t - -let singleton e = S.singleton (Atom e) - -let empty = S.empty - -let union s1 s2 = S.union s1 s2 - -let iter_atoms f s = - S.iter (fun e -> match e with - | Fresh _ -> () - | Atom a -> f a) s - -let fold_atoms f s acc = - S.fold (fun e acc -> match e with - | Fresh _ -> acc - | Atom a -> f a acc) s acc - -let merge e1 e2 = e1 - - -let fresh_exp = - let r = ref (-1) in - fun () -> incr r; !r - -let remove_fresh i s = - let fi = Fresh i in - if S.mem fi s then Some (S.remove fi s) - else None - -let add_fresh i = S.add (Fresh i) - - -let print fmt ex = - fprintf fmt "{"; - S.iter (function - | Atom a -> fprintf fmt "%a, " Debug.atom a - | Fresh i -> fprintf fmt "Fresh%d " i) ex; - fprintf fmt "}" diff --git a/smt/solver_types.mli b/smt/solver_types.mli deleted file mode 100644 index 78a0a230..00000000 --- a/smt/solver_types.mli +++ /dev/null @@ -1,81 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - - - -type var = - { vid : int; - pa : atom; - na : atom; - mutable weight : float; - mutable seen : bool; - mutable level : int; - mutable reason : reason; - mutable vpremise : premise } - -and atom = - { var : var; - lit : Literal.LT.t; - neg : atom; - mutable watched : clause Vec.t; - mutable is_true : bool; - aid : int } - -and clause = - { name : string; - mutable atoms : atom Vec.t; - mutable activity : float; - mutable removed : bool; - learnt : bool; - cpremise : premise } - -and reason = clause option - -and premise = clause list - -module Make (Dummy : sig end) : sig - -val cpt_mk_var : int ref -val ma : var Literal.LT.Map.t ref - -val dummy_var : var -val dummy_atom : atom -val dummy_clause : clause - -val make_var : Literal.LT.t -> var * bool - -val add_atom : Literal.LT.t -> atom - -val make_clause : string -> atom list -> int -> bool -> premise-> clause - -val fresh_name : unit -> string - -val fresh_lname : unit -> string - -val fresh_dname : unit -> string - -val to_float : int -> float - -val to_int : float -> int -val made_vars_info : unit -> int * var list -val clear : unit -> unit - -end - -module Debug: sig - - val atom : Format.formatter -> atom -> unit - - val clause : Format.formatter -> clause -> unit - -end