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

[bugfix] conflict in forgetful propagation

Browse source
This commit is contained in:
Guillaume Bury 2017-01-27 17:56:47 +01:00
parent f82e475a42
commit 44509c6f8d
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/internal.ml
View file

@ -733,7 +733,7 @@ module Make
(* Add a new clause, simplifying, propagating, and backtracking if (* Add a new clause, simplifying, propagating, and backtracking if
the clause is false in the current trail *) the clause is false in the current trail *)
let add_clause ?(force=false) (init:clause) : unit = let add_clause (init:clause) : unit =
Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init); Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init);
let vec = match init.cpremise with let vec = match init.cpremise with
| Hyp -> env.clauses_hyps | Hyp -> env.clauses_hyps
@ -932,7 +932,11 @@ module Make
let p = atom f in let p = atom f in
let c = make_clause (fresh_tname ()) let c = make_clause (fresh_tname ())
(p :: List.map (fun a -> a.neg) l) (Lemma proof) in (p :: List.map (fun a -> a.neg) l) (Lemma proof) in
enqueue_bool p (decision_level ()) (Bcp c) if p.is_true then ()
else if p.neg.is_true then
Stack.push c env.clauses_to_add
else
enqueue_bool p (decision_level ()) (Bcp c)
else else
raise (Invalid_argument "Msat.Internal.slice_propagate") raise (Invalid_argument "Msat.Internal.slice_propagate")