simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Begun Functoring the sat solver.

Browse source 
New folder to distinguish sat solver from smt solver.
This commit is contained in:
Guillaume Bury 2014-10-29 18:51:32 +01:00
parent 580ac25745
commit eb692230d3
13 changed files with 303 additions and 257 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
smt/.merlin → sat/.merlin
View file

70
sat/explanation.ml Normal file
View file

@ -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

24
smt/explanation.mli → sat/explanation.mli
View file

@ -12,26 +12,6 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
type t module type S = Explanation_intf.S
type exp module Make : functor (St : Solver_types.S) -> S with type atom = St.atom
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

35
sat/explanation_intf.ml Normal file
View file

@ -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

40
sat/formula_intf.ml Normal file
View file

@ -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

27
smt/solver.ml → sat/solver.ml
View file

@ -10,11 +10,14 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
open Solver_types
open Format open Format
module Th = Cc.Make(Combine.CX) module Make(F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) = struct
module Ex = Explanation
module Stypes = Solver_types.Make(F)
module Ex = Explanation.Make(Stypes)
open Stypes
exception Sat exception Sat
exception Unsat of clause list exception Unsat of clause list
@ -130,17 +133,12 @@ type env =
exception Conflict of clause exception Conflict of clause
module Make (Dummy : sig end) = struct
module Solver_types = Solver_types.Make(struct end)
open Solver_types
type state = type state =
{ {
env : env; env : env;
st_cpt_mk_var: int; 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); *) (* ignore(Th.expensive_processing env.tenv); *)
(* if D1.d then eprintf "expensive_theory_propagate => None@."; *) (* if D1.d then eprintf "expensive_theory_propagate => None@."; *)
(* None *) (* None *)
(* with Exception.Inconsistent dep -> *) (* with Th.Inconsistent dep -> *)
(* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *) (* if D1.d then eprintf "expensive_theory_propagate => Inconsistent@."; *)
(* Some dep *) (* Some dep *)
@ -436,11 +434,11 @@ let theory_propagate () =
let full_model = nb_assigns() = env.nb_init_vars in let full_model = nb_assigns() = env.nb_init_vars in
env.tenv <- env.tenv <-
List.fold_left 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; env.tenv !facts;
if full_model then expensive_theory_propagate () if full_model then expensive_theory_propagate ()
else None else None
with Exception.Inconsistent dep -> with Th.Inconsistent dep ->
(* eprintf "th inconsistent : %a @." Ex.print dep; *) (* eprintf "th inconsistent : %a @." Ex.print dep; *)
Some dep Some dep
@ -697,12 +695,12 @@ let check_inconsistence_of dep =
let env = ref (Th.empty()) in (); let env = ref (Th.empty()) in ();
Ex.iter_atoms Ex.iter_atoms
(fun atom -> (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) env := t)
dep; dep;
(* ignore (Th.expensive_processing !env); *) (* ignore (Th.expensive_processing !env); *)
assert false assert false
with Exception.Inconsistent _ -> () with Th.Inconsistent _ -> ()
let theory_analyze dep = let theory_analyze dep =
let atoms, sz, max_lvl, c_hist = 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 var, negated = make_var lit in
let truth = var.pa.is_true in let truth = var.pa.is_true in
if negated then not truth else truth if negated then not truth else truth
end end

23
smt/solver.mli → sat/solver.mli
View file

@ -11,18 +11,21 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
exception Sat module Make (F : Formula_intf.S)(Th : Theory_intf.S with type formula = F.t) : sig
exception Unsat of Solver_types.clause list
module Make (Dummy : sig end) : sig module St : Solver_types.S with type formula = F.t
type state
val solve : unit -> unit exception Sat
val assume : Literal.LT.t list list -> cnumber : int -> unit exception Unsat of St.clause list
val clear : unit -> unit
val eval : Literal.LT.t -> bool type state
val save : unit -> state
val restore : state -> unit 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 end

69
smt/solver_types.ml → sat/solver_types.ml
View file

@ -21,6 +21,7 @@ let is_le n = Hstring.compare n ale = 0
let is_lt n = Hstring.compare n alt = 0 let is_lt n = Hstring.compare n alt = 0
let is_gt n = Hstring.compare n agt = 0 let is_gt n = Hstring.compare n agt = 0
module Make (F : Formula_intf.S) = struct
type var = type var =
{ vid : int; { vid : int;
@ -34,7 +35,7 @@ type var =
and atom = and atom =
{ var : var; { var : var;
lit : Literal.LT.t; lit : F.t;
neg : atom; neg : atom;
mutable watched : clause Vec.t; mutable watched : clause Vec.t;
mutable is_true : bool; mutable is_true : bool;
@ -52,9 +53,7 @@ and reason = clause option
and premise = clause list and premise = clause list
module Make (Dummy : sig end) = struct let dummy_lit = F.dummy
let dummy_lit = Literal.LT.make (Literal.Eq(Term.vrai,Term.vrai))
let rec dummy_var = let rec dummy_var =
{ vid = -101; { vid = -101;
@ -80,8 +79,7 @@ and dummy_clause =
learnt = false; learnt = false;
cpremise = [] } cpremise = [] }
module MA = F.Map
module MA = Literal.LT.Map
let ale = Hstring.make "<=" let ale = Hstring.make "<="
let alt = 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_lt n = Hstring.compare n alt = 0
let is_gt n = Hstring.compare n agt = 0 let is_gt n = Hstring.compare n agt = 0
let normal_form lit = let normal_form = F.norm
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 cpt_mk_var = ref 0 let cpt_mk_var = ref 0
let ma = ref MA.empty let ma = ref MA.empty
@ -165,7 +117,7 @@ let make_var =
aid = cpt_fois_2 (* aid = vid*2 *) } aid = cpt_fois_2 (* aid = vid*2 *) }
and na = and na =
{ var = var; { var = var;
lit = Literal.LT.neg lit; lit = F.neg lit;
watched = Vec.make 10 dummy_clause; watched = Vec.make 10 dummy_clause;
neg = pa; neg = pa;
is_true = false; is_true = false;
@ -222,10 +174,6 @@ let clear () =
cpt_mk_var := 0; cpt_mk_var := 0;
ma := MA.empty ma := MA.empty
end
module Debug = struct module Debug = struct
let sign a = if a==a.var.pa then "" else "-" let sign a = if a==a.var.pa then "" else "-"
@ -253,10 +201,9 @@ module Debug = struct
let atom fmt a = let atom fmt a =
fprintf fmt "%s%d%s [lit:%a] vpremise={{%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 premise a.var.vpremise
let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l
let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr 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} = let clause fmt {name=name; atoms=arr; cpremise=cp} =
fprintf fmt "%s:{ %a} cpremise={{%a}}" name atoms_vec arr premise cp fprintf fmt "%s:{ %a} cpremise={{%a}}" name atoms_vec arr premise cp
end
end end

16
sat/solver_types.mli Normal file
View file

@ -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

79
sat/solver_types_intf.ml Normal file
View file

@ -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

27
sat/theory_intf.ml Normal file
View file

@ -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

69
smt/explanation.ml
View file

@ -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 "}"

81
smt/solver_types.mli
View file

@ -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