simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 12:54:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Log module is passed down to proof module in solvers

Browse source
This commit is contained in:
Guillaume Bury 2015-03-13 14:09:16 +01:00
parent 9b41aab1b1
commit d7c5077c0a
6 changed files with 31 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
solver/mcproof.ml
View file

@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S module type S = Res_intf.S
module Make(St : Mcsolver_types.S) = struct module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct
(* Type definitions *) (* Type definitions *)
type lemma = St.proof type lemma = St.proof
@ -80,7 +80,7 @@ module Make(St : Mcsolver_types.S) = struct
let res = List.sort_uniq compare_atoms !l in let res = List.sort_uniq compare_atoms !l in
let l, _ = resolve res in let l, _ = resolve res in
if l <> [] then if l <> [] then
Log.debug 3 "Input clause is a tautology"; L.debug 3 "Input clause is a tautology";
res res
(* Adding hyptoheses *) (* Adding hyptoheses *)
@ -99,9 +99,9 @@ module Make(St : Mcsolver_types.S) = struct
let is_proven c = is_proved (c, to_list c) let is_proven c = is_proved (c, to_list c)
let add_res (c, cl_c) (d, cl_d) = let add_res (c, cl_c) (d, cl_d) =
Log.debug 7 " Resolving clauses :"; L.debug 7 " Resolving clauses :";
Log.debug 7 " %a" St.pp_clause c; L.debug 7 " %a" St.pp_clause c;
Log.debug 7 " %a" St.pp_clause d; L.debug 7 " %a" St.pp_clause d;
assert (is_proved (c, cl_c)); assert (is_proved (c, cl_c));
assert (is_proved (d, cl_d)); assert (is_proved (d, cl_d));
let l = merge cl_c cl_d in let l = merge cl_c cl_d in
@ -111,7 +111,7 @@ module Make(St : Mcsolver_types.S) = struct
| [a] -> | [a] ->
H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); 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]) in let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in
Log.debug 5 "New clause : %a" St.pp_clause new_c; L.debug 5 "New clause : %a" St.pp_clause new_c;
new_c, new_clause new_c, new_clause
| _ -> raise (Resolution_error "Resolved to a tautology") | _ -> raise (Resolution_error "Resolved to a tautology")
@ -133,9 +133,9 @@ module Make(St : Mcsolver_types.S) = struct
let add_clause c cl l = (* We assume that all clauses in l are already proved ! *) let add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
match l with match l with
| a :: r -> | a :: r ->
Log.debug 5 "Resolving (with history) %a" St.pp_clause c; L.debug 5 "Resolving (with history) %a" St.pp_clause c;
let temp_c, temp_cl = List.fold_left add_res a r in let temp_c, temp_cl = List.fold_left add_res a r in
Log.debug 10 " Switching to unit resolutions"; L.debug 10 " Switching to unit resolutions";
let new_c, new_cl = (ref temp_c, ref temp_cl) in let new_c, new_cl = (ref temp_c, ref temp_cl) in
while not (equal_cl cl !new_cl) do while not (equal_cl cl !new_cl) do
let unit_to_use = diff_learnt [] cl !new_cl in let unit_to_use = diff_learnt [] cl !new_cl in
@ -172,14 +172,14 @@ module Make(St : Mcsolver_types.S) = struct
end end
let prove c = let prove c =
Log.debug 3 "Proving : %a" St.pp_clause c; L.debug 3 "Proving : %a" St.pp_clause c;
do_clause [c]; do_clause [c];
Log.debug 3 "Proved : %a" St.pp_clause c L.debug 3 "Proved : %a" St.pp_clause c
let rec prove_unsat_cl (c, cl) = match cl with let rec prove_unsat_cl (c, cl) = match cl with
| [] -> true | [] -> true
| a :: r -> | a :: r ->
Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
let d = match St.(a.var.level, a.var.tag.reason) with let d = match St.(a.var.level, a.var.tag.reason) with
| 0, St.Bcp Some d -> d | 0, St.Bcp Some d -> d
| _ -> raise Exit | _ -> raise Exit
@ -195,11 +195,11 @@ module Make(St : Mcsolver_types.S) = struct
false false
let learn v = let learn v =
Vec.iter (fun c -> Log.debug 15 "history : %a" St.pp_clause c) v; Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v;
Vec.iter prove v Vec.iter prove v
let assert_can_prove_unsat c = let assert_can_prove_unsat c =
Log.debug 1 "=================== Proof ====================="; L.debug 1 "=================== Proof =====================";
prove c; prove c;
if not (prove_unsat_cl (c, to_list c)) then if not (prove_unsat_cl (c, to_list c)) then
raise Insuficient_hyps raise Insuficient_hyps
@ -216,7 +216,7 @@ module Make(St : Mcsolver_types.S) = struct
| Resolution of proof * proof * atom | Resolution of proof * proof * atom
let rec return_proof (c, cl) () = let rec return_proof (c, cl) () =
Log.debug 8 "Returning proof for : %a" St.pp_clause c; L.debug 8 "Returning proof for : %a" St.pp_clause c;
let st = match H.find proof cl with let st = match H.find proof cl with
| Assumption -> Hypothesis | Assumption -> Hypothesis
| Lemma l -> Lemma l | Lemma l -> Lemma l

2
solver/mcproof.mli
View file

@ -6,6 +6,6 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S module type S = Res_intf.S
module Make : functor (St : Mcsolver_types.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 -> 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. *) (** Functor to create a module building proofs from a sat-solver unsat trace. *)

2
solver/mcsolver.ml
View file

@ -8,7 +8,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
(Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
module St = Mcsolver_types.Make(E)(Th) module St = Mcsolver_types.Make(E)(Th)
module Proof = Mcproof.Make(St) module Proof = Mcproof.Make(L)(St)
open St open St

26
solver/res.ml
View file

@ -6,7 +6,7 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S module type S = Res_intf.S
module Make(St : Solver_types.S) = struct module Make(L : Log_intf.S)(St : Solver_types.S) = struct
(* Type definitions *) (* Type definitions *)
type lemma = St.proof type lemma = St.proof
@ -98,9 +98,9 @@ module Make(St : Solver_types.S) = struct
let is_proven c = is_proved (c, to_list c) let is_proven c = is_proved (c, to_list c)
let add_res (c, cl_c) (d, cl_d) = let add_res (c, cl_c) (d, cl_d) =
Log.debug 7 " Resolving clauses :"; L.debug 7 " Resolving clauses :";
Log.debug 7 " %a" St.pp_clause c; L.debug 7 " %a" St.pp_clause c;
Log.debug 7 " %a" St.pp_clause d; L.debug 7 " %a" St.pp_clause d;
assert (is_proved (c, cl_c)); assert (is_proved (c, cl_c));
assert (is_proved (d, cl_d)); assert (is_proved (d, cl_d));
let l = merge cl_c cl_d in let l = merge cl_c cl_d in
@ -110,7 +110,7 @@ module Make(St : Solver_types.S) = struct
| [a] -> | [a] ->
H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); 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]) in let new_c = St.make_clause (fresh_pcl_name ()) new_clause (List.length new_clause) true St.(History [c; d]) in
Log.debug 5 "New clause : %a" St.pp_clause new_c; L.debug 5 "New clause : %a" St.pp_clause new_c;
new_c, new_clause new_c, new_clause
| _ -> raise (Resolution_error "Resolved to a tautology") | _ -> raise (Resolution_error "Resolved to a tautology")
@ -132,9 +132,9 @@ module Make(St : Solver_types.S) = struct
let add_clause c cl l = (* We assume that all clauses in l are already proved ! *) let add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
match l with match l with
| a :: r -> | a :: r ->
Log.debug 5 "Resolving (with history) %a" St.pp_clause c; L.debug 5 "Resolving (with history) %a" St.pp_clause c;
let temp_c, temp_cl = List.fold_left add_res a r in let temp_c, temp_cl = List.fold_left add_res a r in
Log.debug 10 " Switching to unit resolutions"; L.debug 10 " Switching to unit resolutions";
let new_c, new_cl = (ref temp_c, ref temp_cl) in let new_c, new_cl = (ref temp_c, ref temp_cl) in
while not (equal_cl cl !new_cl) do while not (equal_cl cl !new_cl) do
let unit_to_use = diff_learnt [] cl !new_cl in let unit_to_use = diff_learnt [] cl !new_cl in
@ -171,14 +171,14 @@ module Make(St : Solver_types.S) = struct
end end
let prove c = let prove c =
Log.debug 3 "Proving : %a" St.pp_clause c; L.debug 3 "Proving : %a" St.pp_clause c;
do_clause [c]; do_clause [c];
Log.debug 3 "Proved : %a" St.pp_clause c L.debug 3 "Proved : %a" St.pp_clause c
let rec prove_unsat_cl (c, cl) = match cl with let rec prove_unsat_cl (c, cl) = match cl with
| [] -> true | [] -> true
| a :: r -> | a :: r ->
Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; L.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
let d = match St.(a.var.level, a.var.reason) with let d = match St.(a.var.level, a.var.reason) with
| 0, Some d -> d | 0, Some d -> d
| _ -> raise Exit | _ -> raise Exit
@ -194,11 +194,11 @@ module Make(St : Solver_types.S) = struct
false false
let learn v = let learn v =
Vec.iter (fun c -> Log.debug 15 "history : %a" St.pp_clause c) v; Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v;
Vec.iter prove v Vec.iter prove v
let assert_can_prove_unsat c = let assert_can_prove_unsat c =
Log.debug 1 "=================== Proof ====================="; L.debug 1 "=================== Proof =====================";
prove c; prove c;
if not (prove_unsat_cl (c, to_list c)) then if not (prove_unsat_cl (c, to_list c)) then
raise Insuficient_hyps raise Insuficient_hyps
@ -215,7 +215,7 @@ module Make(St : Solver_types.S) = struct
| Resolution of proof * proof * atom | Resolution of proof * proof * atom
let rec return_proof (c, cl) () = let rec return_proof (c, cl) () =
Log.debug 8 "Returning proof for : %a" St.pp_clause c; L.debug 8 "Returning proof for : %a" St.pp_clause c;
let st = match H.find proof cl with let st = match H.find proof cl with
| Assumption -> Hypothesis | Assumption -> Hypothesis
| Lemma l -> Lemma l | Lemma l -> Lemma l

2
solver/res.mli
View file

@ -6,6 +6,6 @@ Copyright 2014 Simon Cruanes
module type S = Res_intf.S module type S = Res_intf.S
module Make : functor (St : Solver_types.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 -> 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. *) (** Functor to create a module building proofs from a sat-solver unsat trace. *)

2
solver/solver.ml
View file

@ -14,7 +14,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t) = struct (Th : Theory_intf.S with type formula = F.t) = struct
module St = Solver_types.Make(F)(Th) module St = Solver_types.Make(F)(Th)
module Proof = Res.Make(St) module Proof = Res.Make(L)(St)
open St open St