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

Better proofs

Browse source 
Proof graphs are now entirely stored in
the cpremise field of clauses
This commit is contained in:
Guillaume Bury 2016-01-21 03:34:18 +01:00
parent 2613926ab1
commit 9a481f6450
8 changed files with 119 additions and 243 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
smt/mcsat.ml
View file

@ -139,7 +139,10 @@ module Make(Dummy:sig end) = struct
(* SmtSolver.Proof.learn (SmtSolver.history ()); *)
match SmtSolver.unsat_conflict () with
| None -> assert false
| Some c -> SmtSolver.Proof.prove_unsat c
| Some c ->
let p = SmtSolver.Proof.prove_unsat c in
SmtSolver.Proof.check p;
p
let eval = SmtSolver.eval

5
smt/smt.ml
View file

@ -89,7 +89,10 @@ module Make(Dummy:sig end) = struct
let get_proof () =
match SmtSolver.unsat_conflict () with
| None -> assert false
| Some c -> SmtSolver.Proof.prove_unsat c
| Some c ->
let p = SmtSolver.Proof.prove_unsat c in
SmtSolver.Proof.check p;
p
let eval = SmtSolver.eval

22
solver/internal.ml
View file

@ -27,7 +27,6 @@ module Make
ul_th_env : Th.level; (* Theory state at level 0 *)
ul_clauses : int; (* number of clauses *)
ul_learnt : int; (* number of learnt clauses *)
ul_proof_lvl : int; (* push/pop index for Res module *)
}
(* Singleton type containing the current state *)
@ -128,7 +127,6 @@ module Make
ul_learnt = 0;
ul_clauses = 0;
ul_th_env = Th.dummy;
ul_proof_lvl = -1;
};
order = Iheap.init 0;
@ -383,6 +381,8 @@ module Make
()
let report_unsat ({atoms=atoms} as confl) =
L.debug 5 "Unsat conflict:";
L.debug 5 " %a" St.pp_clause confl;
env.unsat_conflict <- Some confl;
raise Unsat
@ -393,7 +393,7 @@ module Make
| [ a ] ->
if history = [] then r
else
let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (List.rev (cl :: history))) c_lvl in
let tmp_cl = make_clause (fresh_tname ()) l 1 true (History (cl :: history)) c_lvl in
Bcp (Some tmp_cl)
| _ -> assert false
end
@ -490,7 +490,7 @@ module Make
with Exit ->
let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in
let blevel = backtrack_lvl !is_uip learnt in
blevel, learnt, !history, !is_uip, !c_level
blevel, learnt, List.rev !history, !is_uip, !c_level
let get_atom i =
destruct (Vec.get env.elt_queue i)
@ -552,7 +552,7 @@ module Make
| n, _ -> assert false
done;
List.iter (fun q -> q.var.seen <- false) !seen;
!blevel, !learnt, !history, true, !c_level
!blevel, !learnt, List.rev !history, true, !c_level
let analyze c_clause =
if St.mcsat then
@ -605,9 +605,9 @@ module Make
| History _ -> assert false
in
try
if not force && Proof.has_been_proved init0 then raise Trivial;
if not (Proof.is_proven init0) then assert false; (* Important side-effect, DO NOT REMOVE *)
let atoms, init, level = partition (Vec.to_list init0.atoms) init0.c_level in
(* if not force && Proof.has_been_proved init0 then raise Trivial; *)
(* if not (Proof.is_proven init0) then assert false; (* Important side-effect, DO NOT REMOVE *) *)
let atoms, history, level = partition (Vec.to_list init0.atoms) init0.c_level in
let size = List.length atoms in
match atoms with
| [] ->
@ -1003,8 +1003,7 @@ module Make
in
let ul_clauses = Vec.size env.clauses_hyps in
let ul_learnt = Vec.size env.clauses_learnt in
let ul_proof_lvl = Proof.push () in
Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt; ul_proof_lvl;};
Vec.push env.user_levels {ul_elt_lvl; ul_th_lvl; ul_th_env; ul_clauses; ul_learnt;};
res
end
@ -1081,9 +1080,6 @@ module Make
done;
Vec.shrink env.clauses_hyps (Vec.size env.clauses_hyps - ul.ul_clauses);
(* Backtrack the Proof module *)
Proof.pop ul.ul_proof_lvl;
(* Refresh the known tautologies simplified because of clauses that have been removed *)
let s = Stack.create () in
let new_sz = ref ul.ul_learnt in

291
solver/res.ml
View file

@ -16,43 +16,9 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
type atom = St.atom
type int_cl = clause * St.atom list
type node =
| Assumption
| Lemma of lemma
| Resolution of atom * int_cl * int_cl
(* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
exception Insuficient_hyps
exception Resolution_error of string
(* Proof graph *)
let hash_cl cl =
Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
let equal_cl cl_c cl_d =
try
List.for_all2 (==) cl_c cl_d
with Invalid_argument _ ->
false
module H = Hashtbl.Make(struct
type t = St.atom list
let hash = hash_cl
let equal = equal_cl
end)
let proof : node H.t ref = ref (H.create 1007);;
let push_stack = Vec.make 0 (H.create 0)
let push () =
let res = Vec.size push_stack in
Vec.push push_stack (H.copy !proof);
res
let pop i =
proof := Vec.get push_stack i;
Vec.shrink push_stack (Vec.size push_stack - i)
(* Misc functions *)
let equal_atoms a b = St.(a.aid) = St.(b.aid)
let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
@ -60,7 +26,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
let merge = List.merge compare_atoms
let _c = ref 0
let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c)
let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c)
(* Printing functions *)
let rec print_cl fmt = function
@ -104,164 +70,11 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
L.debug 3 "Input clause is a tautology";
res
(* Printing *)
let print_clause fmt c = print_cl fmt (to_list c)
(* Adding hyptoheses *)
let has_been_proved c = H.mem !proof (to_list c)
let is_proved (c, cl) =
if H.mem !proof cl then
true
else if not St.(c.learnt) then begin
H.add !proof cl Assumption;
true
end else match St.(c.cpremise) with
| St.Lemma p -> H.add !proof cl (Lemma p); true
| St.History _ -> false
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;
assert (is_proved (c, cl_c));
assert (is_proved (d, cl_d));
let l = merge cl_c cl_d in
let resolved, new_clause = resolve l in
match resolved with
| [] -> raise (Resolution_error "No literal to resolve over")
| [a] ->
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;
new_c, new_clause
| _ -> raise (Resolution_error "Resolved to a tautology")
let rec diff_learnt acc l l' =
match l, l' with
| [], _ -> l' @ acc
| a :: r, b :: r' ->
if equal_atoms a b then
diff_learnt acc r r'
else
diff_learnt (b :: acc) l r'
| _ -> raise (Resolution_error "Impossible to derive correct clause")
let clause_unit a = match St.(a.var.level, a.var.reason) with
| 0, St.Bcp Some c -> c, to_list c
| _ ->
raise (Resolution_error "Could not find a reason needed to resolve")
let need_clause (c, cl) =
if is_proved (c, cl) then
[]
else
match St.(c.cpremise) with
| St.History l -> l
| St.Lemma _ -> assert false
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;
let temp_c, temp_cl = List.fold_left add_res a r in
let tmp = diff_learnt [] cl temp_cl in
List.iter (fun a ->
L.debug 0 " -> %a" St.pp_atom a) tmp;
assert (equal_cl cl temp_cl)
(*
while not (equal_cl cl !new_cl) do
let unit_to_use = diff_learnt [] cl !new_cl in
let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
do_clause (List.map fst unit_r);
let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
new_c := temp_c;
new_cl := temp_cl;
done
*)
| _ -> assert false
and do_clause = function
| [] -> ()
| c :: r ->
let cl = to_list c in
match need_clause (c, cl) with
| [] -> do_clause r
| history ->
let history_cl = List.rev_map (fun c -> c, to_list c) history in
let to_prove = List.filter (fun (c, cl) -> not (is_proved (c, cl))) history_cl in
let to_prove = (List.rev_map fst to_prove) in
begin match to_prove with
| [] ->
add_clause c cl history_cl;
do_clause r
| _ -> do_clause (to_prove @ (c :: r))
end
let prove c =
L.debug 3 "Proving : %a" St.pp_clause c;
do_clause [c];
L.debug 3 "Proved : %a" 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;
let d = match St.(a.var.level, a.var.reason) with
| 0, St.Bcp Some d -> d
| _ -> raise Exit
in
prove d;
let cl_d = to_list d in
prove_unsat_cl (add_res (c, cl) (d, cl_d))
let prove_unsat_cl c =
try
prove_unsat_cl c
with Exit ->
false
let learn v =
Vec.iter (fun c -> L.debug 15 "history : %a" St.pp_clause c) v;
Vec.iter prove v
let assert_can_prove_unsat c =
L.debug 1 "=================== Proof =====================";
prove c;
if not (prove_unsat_cl (c, to_list c)) then
raise Insuficient_hyps
(* Interface exposed *)
type proof = {
table : node H.t;
clause : clause * atom list;
}
and proof_node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis
| Lemma of lemma
| Resolution of proof * proof * atom
let expand { clause = (c, cl); table; } =
let st = match H.find table cl with
| Assumption -> Hypothesis
| Lemma l -> Lemma l
| Resolution (a, cl_c, cl_d) ->
Resolution ({ clause = cl_c; table}, {clause = cl_d; table}, a)
in
{ conclusion = c; step = st }
let prove_unsat c =
assert_can_prove_unsat c;
{clause = St.empty_clause, []; table = !proof; }
(* Compute unsat-core *)
let compare_cl c d =
(* Comparison of clauses *)
let cmp_cl c d =
let rec aux = function
| [], [] -> 0
| a :: r, a' :: r' -> begin match compare_atoms a a' with
@ -271,8 +84,77 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
| _ :: _ , [] -> -1
| [], _ :: _ -> 1
in
aux (to_list c, to_list d)
aux (c, d)
let cmp c d =
cmp_cl (to_list c) (to_list d)
let prove conclusion =
assert St.(conclusion.learnt || conclusion.cpremise <> History []);
conclusion
let prove_unsat c =
let l = Vec.to_list c.St.atoms in
let l = List.map (fun a ->
match St.(a.var.reason) with
| St.Bcp Some d -> d
| _ -> assert false) l
in
St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
(List.fold_left (fun i c -> max i c.St.c_level) 0 l)
(* Interface exposed *)
type proof = clause
and proof_node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis
| Lemma of lemma
| Resolution of proof * proof * atom
let rec chain_res (c, cl) = function
| d :: r ->
L.debug 10 " Resolving :";
L.debug 10 " - %a" St.pp_clause c;
L.debug 10 " - %a" St.pp_clause d;
let dl = to_list d in
begin match resolve (merge cl dl) with
| [ a ], l ->
begin match r with
| [] -> (l, c, d, a)
| _ ->
let new_clause = St.make_clause (fresh_pcl_name ()) l (List.length l) true
(St.History [c; d]) (max c.St.c_level d.St.c_level) in
chain_res (new_clause, l) r
end
| _ -> assert false
end
| _ -> assert false
let rec expand conclusion =
L.debug 5 "Expanding : %a" St.pp_clause conclusion;
match conclusion.St.cpremise with
| St.Lemma l ->
{conclusion; step = Lemma l; }
| St.History [] ->
assert (not conclusion.St.learnt);
{ conclusion; step = Hypothesis; }
| St.History [ c ] ->
assert (cmp c conclusion = 0);
expand c
| St.History ( c :: ([d] as r)) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
| St.History ( c :: r ) ->
let (l, c', d', a) = chain_res (c, to_list c) r in
conclusion.St.cpremise <- St.History [c'; d'];
assert (cmp_cl l (to_list conclusion) = 0);
{ conclusion; step = Resolution (c', d', a); }
(* Compute unsat-core *)
let unsat_core proof =
let rec aux acc proof =
let p = expand proof in
@ -281,9 +163,16 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
| Resolution (proof1, proof2, _) ->
aux (aux acc proof1) proof2
in
sort_uniq compare_cl (aux [] proof)
sort_uniq cmp (aux [] proof)
(* Iter on proofs *)
module H = Hashtbl.Make(struct
type t = clause
let hash cl =
Vec.fold (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms
let equal = (==)
end)
type task =
| Enter of proof
| Leaving of proof
@ -293,13 +182,13 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
let rec fold_aux s h f acc =
match spop s with
| None -> acc
| Some (Leaving ({clause = (_, cl)} as p)) ->
H.add h cl true;
fold_aux s h f (f acc (expand p))
| Some (Enter ({clause = (_, cl)} as p)) ->
if not (H.mem h cl) then begin
Stack.push (Leaving p) s;
let node = expand p in
| Some (Leaving c) ->
H.add h c true;
fold_aux s h f (f acc (expand c))
| Some (Enter c) ->
if not (H.mem h c) then begin
Stack.push (Leaving c) s;
let node = expand c in
begin match node.step with
| Resolution (p1, p2, _) ->
Stack.push (Enter p2) s;
@ -315,5 +204,7 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
Stack.push (Enter p) s;
fold_aux s h f acc
let check p = fold (fun () _ -> ()) () p
end

7
solver/res.mli
View file

@ -8,9 +8,6 @@ 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
val pop : int -> unit
end
functor (St : Solver_types.S) ->
S with module St = St
(** Functor to create a module building proofs from a sat-solver unsat trace. *)

28
solver/res_intf.ml
View file

@ -45,29 +45,11 @@ module type S = sig
(** {3 Proof building functions} *)
val has_been_proved : clause -> bool
(** Returns [true] if the clause is part of the current proof graph. This function does not alter
the proof graph (contrary to [is_proven]). *)
val is_proven : clause -> bool
(** Checks if the given clause has a derivation in the current state. Whatever the result,
new proven clauses (including the given clause) may be added to the proof graph. In particular,
hyptohesis and theory lemmas always have trivial derivations, and as such [is_proven c] (where [c]
is a hypothesis or lemma) will always return [true] and add it to the proof graph. *)
val prove : clause -> unit
val prove : clause -> proof
(** Same as 'learn', but works on single clauses instead of vectors. *)
val learn : clause Vec.t -> unit
(** Learn and build proofs for the clause in the vector. Clauses in the vector should be in the order they were learned. *)
val assert_can_prove_unsat : clause -> unit
(** [assert_can_prove_unsat c] tries and prove the empty clause from [c]. [c] may be a learnt clause not yet proved.
@raise Insuficient_hyps if it is impossible. *)
val prove_unsat : clause -> proof
(** Given a conflict clause [c], returns a proof of the empty clause. Same as [assert_can_prove_unsat] but returns
the proof if it succeeds.
(** Given a conflict clause [c], returns a proof of the empty clause.
@raise Insuficient_hyps if it does not succeed. *)
(** {3 Proof Manipulation} *)
@ -81,10 +63,14 @@ module type S = sig
[f] on a proof node happens after the execution on the children of the nodes. *)
val unsat_core : proof -> clause list
(** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)
(** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof.
More efficient than using the [fold] function since it has access to the internal representation of proofs *)
(** {3 Misc} *)
val check : proof -> unit
(** Check the contents of a proof. Mainly for internal use *)
val print_clause : Format.formatter -> clause -> unit
(** A nice looking printer for clauses, which sort the atoms before printing. *)

2
solver/solver_types.ml
View file

@ -59,8 +59,8 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S) = struct
tag : int option;
atoms : atom Vec.t;
learnt : bool;
cpremise : premise;
c_level : int;
mutable cpremise : premise;
mutable activity : float;
mutable removed : bool;
}

2
solver/solver_types_intf.ml
View file

@ -54,8 +54,8 @@ module type S = sig
tag : int option;
atoms : atom Vec.t;
learnt : bool;
cpremise : premise;
c_level : int;
mutable cpremise : premise;
mutable activity : float;
mutable removed : bool;
}