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

for proofs, represent assumptions as propagations

Browse source
This commit is contained in:
Simon Cruanes 2016-07-28 10:56:19 +02:00
parent eb14a1e229
commit 5a04fa49ed
4 changed files with 6 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/core/internal.ml
View file

@ -287,7 +287,7 @@ module Make
if a.neg.is_true then begin if a.neg.is_true then begin
(* If a variable is false, we need to see why it is false. *) (* If a variable is false, we need to see why it is false. *)
match a.var.reason with match a.var.reason with
| None | Some Decision | Some Assumption -> assert false | None | Some Decision -> assert false
(* The var must have a reason, and it cannot be a decision/assumption, since we are (* The var must have a reason, and it cannot be a decision/assumption, since we are
at level 0. *) at level 0. *)
| Some (Bcp cl) -> atoms, cl :: history | Some (Bcp cl) -> atoms, cl :: history
@ -620,7 +620,7 @@ module Make
c := res c := res
| _ -> assert false | _ -> assert false
end end
| None | Some Decision | Some Assumption | Some Semantic _ -> () | None | Some Decision | Some Semantic _ -> ()
end end
done; assert false done; assert false
with Exit -> with Exit ->
@ -1110,7 +1110,8 @@ module Make
let level = decision_level() in let level = decision_level() in
assert (env.base_level = level-1); assert (env.base_level = level-1);
env.base_level <- level; env.base_level <- level;
enqueue_bool a ~level Assumption; let c = make_clause (fresh_hname ()) [a] Hyp in
enqueue_bool a ~level (Bcp c);
match propagate () with match propagate () with
| Some confl -> (* Conflict *) | Some confl -> (* Conflict *)
report_unsat confl; report_unsat confl;

4
src/core/res.ml
View file

@ -136,7 +136,7 @@ module Make(St : Solver_types.S) = struct
match conclusion.St.cpremise with match conclusion.St.cpremise with
| St.Lemma l -> | St.Lemma l ->
{conclusion; step = Lemma l; } {conclusion; step = Lemma l; }
| St.Hyp _ -> | St.Hyp ->
{ conclusion; step = Hypothesis; } { conclusion; step = Hypothesis; }
| St.History [] -> | St.History [] ->
assert false assert false
@ -163,7 +163,7 @@ module Make(St : Solver_types.S) = struct
if not c.St.visited then begin if not c.St.visited then begin
c.St.visited <- true; c.St.visited <- true;
match c.St.cpremise with match c.St.cpremise with
| St.Hyp _ | St.Lemma _ -> aux (c :: res) acc r | St.Hyp | St.Lemma _ -> aux (c :: res) acc r
| St.History h -> | St.History h ->
let l = List.fold_left (fun acc c -> let l = List.fold_left (fun acc c ->
if not c.St.visited then c :: acc else acc) r h in if not c.St.visited then c :: acc else acc) r h in

2
src/core/solver_types.ml
View file

@ -68,7 +68,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| Decision | Decision
| Bcp of clause | Bcp of clause
| Semantic of int | Semantic of int
| Assumption
and premise = and premise =
| Hyp | Hyp
@ -267,7 +266,6 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
| n, Some Decision -> sprintf "@@%d" n | n, Some Decision -> sprintf "@@%d" n
| n, Some Bcp c -> sprintf "->%d/%s" n c.name | n, Some Bcp c -> sprintf "->%d/%s" n c.name
| n, Some Semantic lvl -> sprintf "::%d/%d" n lvl | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl
| n, Some Assumption -> sprintf "!%d" n
let value a = let value a =
if a.is_true then sprintf "[T%s]" (level a) if a.is_true then sprintf "[T%s]" (level a)

1
src/core/solver_types_intf.ml
View file

@ -63,7 +63,6 @@ module type S = sig
| Decision | Decision
| Bcp of clause | Bcp of clause
| Semantic of int | Semantic of int
| Assumption
and premise = and premise =
| Hyp | Hyp