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

Fix for dependencies during proof computing

Browse source
This commit is contained in:
Guillaume Bury 2015-03-13 15:03:30 +01:00
parent ee13eb366b
commit 5047882fc7
5 changed files with 25 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
sat/sat.ml
View file

@ -141,8 +141,7 @@ module Make(Log : Log_intf.S) = struct
let eval = SatSolver.eval let eval = SatSolver.eval
let get_proof () = let get_proof () =
SatSolver.Proof.learn (SatSolver.hyps ()); (* SatSolver.Proof.learn (SatSolver.history ()); *)
SatSolver.Proof.learn (SatSolver.history ());
match SatSolver.unsat_conflict () with match SatSolver.unsat_conflict () with
| None -> assert false | None -> assert false
| Some c -> SatSolver.Proof.prove_unsat c | Some c -> SatSolver.Proof.prove_unsat c

3
smt/mcsat.ml
View file

@ -135,8 +135,7 @@ module Make(Dummy:sig end) = struct
with SmtSolver.Unsat -> () with SmtSolver.Unsat -> ()
let get_proof () = let get_proof () =
SmtSolver.Proof.learn (SmtSolver.hyps ()); (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
SmtSolver.Proof.learn (SmtSolver.history ());
match SmtSolver.unsat_conflict () with match SmtSolver.unsat_conflict () with
| None -> assert false | None -> assert false
| Some c -> SmtSolver.Proof.prove_unsat c | Some c -> SmtSolver.Proof.prove_unsat c

3
smt/smt.ml
View file

@ -84,8 +84,7 @@ module Make(Dummy:sig end) = struct
with SmtSolver.Unsat -> () with SmtSolver.Unsat -> ()
let get_proof () = let get_proof () =
SmtSolver.Proof.learn (SmtSolver.hyps ()); (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
SmtSolver.Proof.learn (SmtSolver.history ());
match SmtSolver.unsat_conflict () with match SmtSolver.unsat_conflict () with
| None -> assert false | None -> assert false
| Some c -> SmtSolver.Proof.prove_unsat c | Some c -> SmtSolver.Proof.prove_unsat c

21
solver/mcproof.ml
View file

@ -130,7 +130,15 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct
| _ -> | _ ->
raise (Resolution_error "Could not find a reason needed to resolve") raise (Resolution_error "Could not find a reason needed to resolve")
let add_clause c cl l = (* We assume that all clauses in l are already proved ! *) 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 match l with
| a :: r -> | a :: r ->
L.debug 5 "Resolving (with history) %a" St.pp_clause c; L.debug 5 "Resolving (with history) %a" St.pp_clause c;
@ -140,21 +148,14 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct
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
let unit_r = List.map (fun a -> clause_unit a) unit_to_use 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 let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
new_c := temp_c; new_c := temp_c;
new_cl := temp_cl; new_cl := temp_cl;
done done
| _ -> assert false | _ -> assert false
let need_clause (c, cl) = and do_clause = function
if is_proved (c, cl) then
[]
else
match St.(c.cpremise) with
| St.History l -> l
| St.Lemma _ -> assert false
let rec do_clause = function
| [] -> () | [] -> ()
| c :: r -> | c :: r ->
let cl = to_list c in let cl = to_list c in

21
solver/res.ml
View file

@ -129,7 +129,15 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
| _ -> | _ ->
raise (Resolution_error "Could not find a reason needed to resolve") raise (Resolution_error "Could not find a reason needed to resolve")
let add_clause c cl l = (* We assume that all clauses in l are already proved ! *) 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 match l with
| a :: r -> | a :: r ->
L.debug 5 "Resolving (with history) %a" St.pp_clause c; L.debug 5 "Resolving (with history) %a" St.pp_clause c;
@ -139,21 +147,14 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
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
let unit_r = List.map (fun a -> clause_unit a) unit_to_use 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 let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
new_c := temp_c; new_c := temp_c;
new_cl := temp_cl; new_cl := temp_cl;
done done
| _ -> assert false | _ -> assert false
let need_clause (c, cl) = and do_clause = function
if is_proved (c, cl) then
[]
else
match St.(c.cpremise) with
| St.History l -> l
| St.Lemma _ -> assert false
let rec do_clause = function
| [] -> () | [] -> ()
| c :: r -> | c :: r ->
let cl = to_list c in let cl = to_list c in