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

everwhere, use new Log interface and remove the functor on Log_intf

Browse source
This commit is contained in:
Simon Cruanes 2016-01-20 21:05:22 +01:00
parent 2fe5be8317
commit 756363ffd6
18 changed files with 98 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sat/sat.ml
View file

@ -88,9 +88,9 @@ module Tsat = struct
end
module Make(Log : Log_intf.S) = struct
module Make(Dummy : sig end) = struct
module SatSolver = Solver.Make(Log)(Fsat)(Tsat)
module SatSolver = Solver.Make(Fsat)(Tsat)
module Dot = Dot.Make(SatSolver.Proof)(struct
let clause_name c = SatSolver.St.(c.name)
let print_atom = SatSolver.St.print_atom

2
sat/sat.mli
View file

@ -8,7 +8,7 @@ module Fsat : Formula_intf.S with type t = private int
module Tseitin : Tseitin.S with type atom = Fsat.t
module Make(Log: Log_intf.S) : sig
module Make(Dummy : sig end) : sig
(** Fonctor to make a pure SAT Solver module with built-in literals. *)
exception Bad_atom

9
smt/mcsat.ml
View file

@ -49,8 +49,9 @@ module Tsmt = struct
let current_level () = !env
let to_clause (a, b, l) =
Log.debug 10 "Expl : %s; %s" a b;
List.iter (fun s -> Log.debug 10 " |- %s" s) l;
Log.debugf 10 "@[<2>Expl : %s; %s@ %a@]"
(fun k->k a b
(fun out () -> List.iter (Format.fprintf out " |- %s@ ") l) ());
let rec aux acc = function
| [] | [_] -> acc
| x :: ((y :: _) as r) ->
@ -65,7 +66,7 @@ module Tsmt = struct
| (Assign (x, v)), lvl ->
env := { !env with assign = M.add x (v, lvl) !env.assign }
| Lit f, _ ->
Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f);
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print f);
match f with
| Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) ->
@ -110,7 +111,7 @@ end
module Make(Dummy:sig end) = struct
module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)
module Dot = Dot.Make(SmtSolver.Proof)(struct
let print_atom = SmtSolver.St.print_atom
let lemma_info () = "Proof", Some "PURPLE", []

9
smt/smt.ml
View file

@ -31,8 +31,9 @@ module Tsmt = struct
let current_level () = !env
let to_clause (a, b, l) =
Log.debug 10 "Expl : %s; %s" a b;
List.iter (fun s -> Log.debug 10 " |- %s" s) l;
Log.debugf 10 "@[Expl : %s; %s@ %a@]"
(fun k->k a b
(fun out () -> List.iter (Format.fprintf out "|- %s@ ") l) ());
let rec aux acc = function
| [] | [_] -> acc
| x :: ((y :: _) as r) ->
@ -43,7 +44,7 @@ module Tsmt = struct
let assume s =
try
for i = s.start to s.start + s.length - 1 do
Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print (s.get i));
Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i));
match s.get i with
| Fsmt.Prop _ -> ()
| Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
@ -60,7 +61,7 @@ end
module Make(Dummy:sig end) = struct
module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt)
module SmtSolver = Solver.Make(Fsmt)(Tsmt)
module Dot = Dot.Make(SmtSolver.Proof)(struct
let clause_name c = SmtSolver.St.(c.name)
let print_atom = SmtSolver.St.print_atom

49
solver/internal.ml
View file

@ -5,12 +5,11 @@ Copyright 2014 Simon Cruanes
*)
module Make
(L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
= struct
module Proof = Res.Make(L)(St)
module Proof = Res.Make(St)
open St
@ -268,7 +267,8 @@ module Make
| Bcp (Some cl) -> atoms, false, max lvl cl.c_level
| Semantic 0 -> atoms, init, lvl
| _ ->
L.debug 0 "Unexpected semantic propagation at level 0: %a" St.pp_atom a;
Log.debugf 0 "Unexpected semantic propagation at level 0: %a"
(fun k->k St.pp_atom a);
assert false
end else
a::atoms, init, lvl
@ -334,7 +334,7 @@ module Make
env.clauses_literals <- env.clauses_literals + Vec.size c.atoms
let detach_clause c =
L.debug 10 "Removing clause %a" St.pp_clause c;
Log.debugf 10 "Removing clause @[%a@]" (fun k->k St.pp_clause c);
c.removed <- true;
(* Not necessary, cleanup is done during propagation
Vec.remove (Vec.get c.atoms 0).neg.watched c;
@ -388,7 +388,7 @@ module Make
let enqueue_bool a lvl reason =
if a.neg.is_true then begin
L.debug 0 "Trying to enqueue a false litteral: %a" St.pp_atom a;
Log.debugf 0 "Trying to enqueue a false litteral: %a" (fun k->k St.pp_atom a);
assert false
end;
if not a.is_true then begin
@ -397,7 +397,8 @@ module Make
a.var.level <- lvl;
a.var.reason <- reason;
Vec.push env.elt_queue (of_atom a);
L.debug 20 "Enqueue (%d): %a" (Vec.size env.elt_queue) pp_atom a
Log.debugf 20 "Enqueue (%d): %a"
(fun k->k (Vec.size env.elt_queue) pp_atom a)
end
let enqueue_assign v value lvl =
@ -450,7 +451,7 @@ module Make
raise Exit
| _ ->
decr tr_ind;
L.debug 20 "Looking at trail element %d" !tr_ind;
Log.debugf 20 "Looking at trail element %d" (fun k->k !tr_ind);
destruct (Vec.get env.elt_queue !tr_ind)
(fun _ -> ()) (* TODO remove *)
(fun a -> match a.var.reason with
@ -585,14 +586,14 @@ module Make
let size = List.length atoms in
match atoms with
| [] ->
L.debug 1 "New clause (unsat) : %a" St.pp_clause init0;
Log.debugf 1 "New clause (unsat) :@ @[%a@]" (fun k->k St.pp_clause init0);
report_unsat init0
| a::b::_ ->
let clause =
if init then init0
else make_clause ?tag:init0.tag (fresh_name ()) atoms size true (History [init0]) level
in
L.debug 4 "New clause: %a" St.pp_clause clause;
Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);
attach_clause clause;
Vec.push vec clause;
if a.neg.is_true then begin
@ -605,10 +606,11 @@ module Make
enqueue_bool a lvl (Bcp (Some clause))
end
| [a] ->
L.debug 5 "New unit clause, propagating : %a" St.pp_atom a;
Log.debugf 5 "New unit clause, propagating : %a" (fun k->k St.pp_atom a);
cancel_until 0;
enqueue_bool a 0 (Bcp (Some init0))
with Trivial -> L.debug 5 "Trivial clause ignored : %a" St.pp_clause init0
with Trivial ->
Log.debugf 5 "Trivial clause ignored : @[%a@]" (fun k->k St.pp_clause init0)
let propagate_in_clause a c i watched new_sz =
let atoms = c.atoms in
@ -987,7 +989,7 @@ module Make
(* Backtrack to decision_level 0, with trail_lim && theory env specified *)
let reset_until push_lvl elt_lvl th_lvl th_env =
L.debug 1 "Resetting to decision level 0 (pop/forced)";
Log.debug 1 "Resetting to decision level 0 (pop/forced)";
env.th_head <- th_lvl;
env.elt_head <- elt_lvl;
for c = env.elt_head to Vec.size env.elt_queue - 1 do
@ -1041,14 +1043,19 @@ module Make
reset_until l ul.ul_elt_lvl ul.ul_th_lvl ul.ul_th_env;
(* Log current assumptions for debugging purposes *)
L.debug 99 "Current trail:";
for i = 0 to Vec.size env.elt_queue - 1 do
L.debug 99 "%s%s%d -- %a"
(if i = ul.ul_elt_lvl then "*" else " ")
(if i = ul.ul_th_lvl then "*" else " ")
i (fun fmt e ->
destruct e (St.pp_lit fmt) (St.pp_atom fmt)) (Vec.get env.elt_queue i)
done;
Log.debugf 99 "@[<v2>Current trail:@ %a@]"
(fun k->
let pp out () =
for i = 0 to Vec.size env.elt_queue - 1 do
Format.fprintf out "%s%s%d -- %a@,"
(if i = ul.ul_elt_lvl then "*" else " ")
(if i = ul.ul_th_lvl then "*" else " ")
i (fun fmt e ->
destruct e (St.pp_lit fmt) (St.pp_atom fmt))
(Vec.get env.elt_queue i)
done
in
k pp ());
(* Clear hypothesis not valid anymore *)
for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do
@ -1072,7 +1079,7 @@ module Make
| History [ { cpremise = Lemma _ } as c' ] -> Stack.push c' s
| _ -> () (* Only simplified clauses can have a level > 0 *)
end else begin
L.debug 15 "Keeping intact clause %a" St.pp_clause c;
Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c);
Vec.set env.clauses_learnt !new_sz c;
incr new_sz
end

1
solver/internal.mli
View file

@ -5,7 +5,6 @@ Copyright 2014 Simon Cruanes
*)
module Make
(L : Log_intf.S)
(St : Solver_types.S)
(Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
: sig

6
solver/log_intf.ml
View file

@ -1,6 +0,0 @@
module type S = sig
val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a
(** debug message *)
end

6
solver/mcsolver.ml
View file

@ -4,12 +4,12 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make (L : Log_intf.S)(E : Expr_intf.S)
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) = struct
module St = Solver_types.McMake(L)(E)
module St = Solver_types.McMake(E)
module M = Internal.Make(L)(St)(Th)
module M = Internal.Make(St)(Th)
include St

2
solver/mcsolver.mli
View file

@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make (L : Log_intf.S)(E : Expr_intf.S)
module Make (E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) : sig
(** Functor to create a solver parametrised by the atomic formulas and a theory. *)

30
solver/res.ml
View file

@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S
module Make(L : Log_intf.S)(St : Solver_types.S) = struct
module Make(St : Solver_types.S) = struct
module St = St
@ -65,8 +65,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
(* Printing functions *)
let rec print_cl fmt = function
| [] -> Format.fprintf fmt "[]"
| [a] -> St.print_atom fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r
| [a] -> St.pp_atom fmt a
| a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.pp_atom a print_cl r
(* Compute resolution of 2 clauses *)
let resolve l =
@ -101,7 +101,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
let res = sort_uniq compare_atoms !l in
let l, _ = resolve res in
if l <> [] then
L.debug 3 "Input clause is a tautology";
Log.debug 3 "Input clause is a tautology";
res
let print_clause fmt c = print_cl fmt (to_list c)
@ -122,9 +122,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
let is_proven c = is_proved (c, to_list c)
let add_res (c, cl_c) (d, cl_d) =
L.debug 7 " Resolving clauses :";
L.debug 7 " %a" St.pp_clause c;
L.debug 7 " %a" St.pp_clause d;
Log.debugf 7 "@[<v4> Resolving clauses : %a@,%a@]"
(fun k->k St.pp_clause c St.pp_clause d);
assert (is_proved (c, cl_c));
assert (is_proved (d, cl_d));
let l = merge cl_c cl_d in
@ -135,7 +134,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
H.add !proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause)
true St.(History [c; d]) (max c.St.c_level d.St.c_level) in
L.debug 5 "New clause : %a" St.pp_clause new_c;
Log.debugf 5 "@[<2>New clause :@ @[%a@]@]" (fun k->k St.pp_clause new_c);
new_c, new_clause
| _ -> raise (Resolution_error "Resolved to a tautology")
@ -165,9 +164,9 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
match l with
| a :: r ->
L.debug 5 "Resolving (with history) %a" St.pp_clause c;
Log.debugf 5 "Resolving (with history) %a" (fun k->k St.pp_clause c);
let temp_c, temp_cl = List.fold_left add_res a r in
L.debug 10 " Switching to unit resolutions";
Log.debug 10 " Switching to unit resolutions";
let new_c, new_cl = (ref temp_c, ref temp_cl) in
while not (equal_cl cl !new_cl) do
let unit_to_use = diff_learnt [] cl !new_cl in
@ -197,14 +196,14 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
end
let prove c =
L.debug 3 "Proving : %a" St.pp_clause c;
Log.debugf 3 "Proving : %a" (fun k->k St.pp_clause c);
do_clause [c];
L.debug 3 "Proved : %a" St.pp_clause c
Log.debugf 3 "Proved : %a" (fun k->k St.pp_clause c)
let rec prove_unsat_cl (c, cl) = match cl with
| [] -> true
| a :: r ->
L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
Log.debugf 2 "Eliminating %a in %a" (fun k->k St.pp_atom a St.pp_clause c);
let d = match St.(a.var.level, a.var.reason) with
| 0, St.Bcp Some d -> d
| _ -> raise Exit
@ -220,11 +219,12 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
false
let learn v =
Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v;
Log.debugf 15 "@[<2>history : @[<v>%a@]@]"
(fun k->k (Vec.print ~sep:"" St.pp_clause) v);
Vec.iter prove v
let assert_can_prove_unsat c =
L.debug 1 "=================== Proof =====================";
Log.debug 1 "=================== Proof =====================";
prove c;
if not (prove_unsat_cl (c, to_list c)) then
raise Insuficient_hyps

1
solver/res.mli
View file

@ -7,7 +7,6 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S
module Make :
functor (L : Log_intf.S) ->
functor (St : Solver_types.S) -> sig
include S with module St = St
val push : unit -> int

6
solver/solver.ml
View file

@ -10,7 +10,7 @@
(* *)
(**************************************************************************)
module Make (L : Log_intf.S)(E : Formula_intf.S)
module Make (E : Formula_intf.S)
(Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
module Plugin = struct
@ -70,9 +70,9 @@ module Make (L : Log_intf.S)(E : Formula_intf.S)
let proof_debug _ = assert false
end
module St = Solver_types.SatMake(L)(E)
module St = Solver_types.SatMake(E)
module S = Internal.Make(L)(St)(Plugin)
module S = Internal.Make(St)(Plugin)
include S

2
solver/solver.mli
View file

@ -11,7 +11,7 @@
(* *)
(**************************************************************************)
module Make (L : Log_intf.S)(F : Formula_intf.S)
module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : sig
(** Functor to create a SMT Solver parametrised by the atomic
formulas and a theory. *)

39
solver/solver_types.ml
View file

@ -18,7 +18,7 @@ module type S = Solver_types_intf.S
(* Solver types for McSat Solving *)
(* ************************************************************************ *)
module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
module McMake (E : Expr_intf.S) = struct
(* Flag for Mcsat v.s Pure Sat *)
let mcsat = true
@ -271,29 +271,28 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
else if a.neg.is_true then sprintf "[F%s]" (level a)
else "[]"
let pp_premise b = function
| History v -> List.iter (fun {name=name} -> bprintf b "%s," name) v
| Lemma _ -> bprintf b "th_lemma"
let pp_premise out = function
| History v -> List.iter (fun {name=name} -> Format.fprintf out "%s,@," name) v
| Lemma _ -> Format.fprintf out "th_lemma"
let pp_assign b = function
let pp_assign out = function
| None -> ()
| Some t -> bprintf b "[assignment: %s]" (Log.on_fmt E.Term.print t)
| Some t -> Format.fprintf out "[assignment: %a]" E.Term.print t
let pp_lit b v =
bprintf b "%d [lit:%s]%a"
(v.lid+1) (Log.on_fmt E.Term.print v.term) pp_assign v.assigned
let pp_lit out v =
Format.fprintf out "%d [lit:%a]%a"
(v.lid+1) E.Term.print v.term pp_assign v.assigned
let pp_atom b a =
bprintf b "%s%d%s[lit:%s]"
(sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)
let pp_atom out a =
Format.fprintf out "%s%d%s[lit:%a]"
(sign a) (a.var.vid+1) (value a) E.Formula.print a.lit
let pp_atoms_vec b vec =
for i = 0 to Vec.size vec - 1 do
bprintf b "%a ; " pp_atom (Vec.get vec i)
done
let pp_atoms_vec out vec =
Vec.print ~sep:"; " pp_atom out vec
let pp_clause b {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
bprintf b "%s%s{ %a} cpremise={{%a}}" name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
let pp_clause out {name=name; atoms=arr; cpremise=cp; learnt=learnt} =
Format.fprintf out "%s%s{ %a} cpremise={{%a}}"
name (if learnt then "!" else ":") pp_atoms_vec arr pp_premise cp
end
@ -301,8 +300,8 @@ end
(* Solver types for pure SAT Solving *)
(* ************************************************************************ *)
module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
include McMake(L)(struct
module SatMake (E : Formula_intf.S) = struct
include McMake(struct
include E
module Term = E
module Formula = E

2
solver/solver_types.mli
View file

@ -14,13 +14,11 @@
module type S = Solver_types_intf.S
module McMake :
functor (L : Log_intf.S) ->
functor (E : Expr_intf.S) ->
S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
(** Functor to instantiate the types of clauses for a solver. *)
module SatMake :
functor (L : Log_intf.S) ->
functor (E : Formula_intf.S) ->
S with type term = E.t and type formula = E.t and type proof = E.proof
(** Functor to instantiate the types of clauses for a solver. *)

6
solver/solver_types_intf.ml
View file

@ -134,9 +134,9 @@ module type S = sig
val print_clause : Format.formatter -> clause -> unit
(** Pretty printing functions for atoms and clauses *)
val pp_lit : Buffer.t -> lit -> unit
val pp_atom : Buffer.t -> atom -> unit
val pp_clause : Buffer.t -> clause -> unit
val pp_lit : Format.formatter -> lit -> unit
val pp_atom : Format.formatter -> atom -> unit
val pp_clause : Format.formatter -> clause -> unit
(** Debug function for atoms and clauses (very verbose) *)
end

8
util/vec.ml
View file

@ -161,6 +161,14 @@ let for_all p t =
true
with ExitVec -> false
let print ?(sep=", ") pp out v =
let first = ref true in
iter
(fun x ->
if !first then first := false else Format.fprintf out "%s@," sep;
pp out x)
v
(*
template<class V, class T>
static inline void remove(V& ts, const T& t)

4
util/vec.mli
View file

@ -100,3 +100,7 @@ val exists : ('a -> bool) -> 'a t -> bool
val for_all : ('a -> bool) -> 'a t -> bool
(** Do all elements satisfy the predicate? *)
val print :
?sep:string ->
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit