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

Renamed new_atom -> create_atom

Browse source
This commit is contained in:
Guillaume Bury 2017-01-24 10:53:34 +01:00
parent ee6c61086a
commit 1f5b5fc422
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/internal.ml
View file

@ -886,7 +886,7 @@ module Make
() ()
(* Propagation (boolean and theory) *) (* Propagation (boolean and theory) *)
let new_atom f = let create_atom f =
let a = atom f in let a = atom f in
ignore (th_eval a); ignore (th_eval a);
a a
@ -900,7 +900,7 @@ module Make
| Lit _ -> assert false | Lit _ -> assert false
let slice_push (l:formula list) (lemma:proof): unit = let slice_push (l:formula list) (lemma:proof): unit =
let atoms = List.rev_map (fun x -> new_atom x) l in let atoms = List.rev_map create_atom l in
let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in let c = make_clause (fresh_tname ()) atoms (Lemma lemma) in
Log.debugf info "Pushing clause %a" (fun k->k St.pp_clause c); Log.debugf info "Pushing clause %a" (fun k->k St.pp_clause c);
(* do not add the clause yet, wait for the theory propagation to (* do not add the clause yet, wait for the theory propagation to
@ -954,7 +954,7 @@ module Make
propagate () propagate ()
| Plugin_intf.Unsat (l, p) -> | Plugin_intf.Unsat (l, p) ->
(* conflict *) (* conflict *)
let l = List.rev_map new_atom l in let l = List.rev_map create_atom l in
Iheap.grow_to_at_least env.order (St.nb_elt ()); Iheap.grow_to_at_least env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
@ -1125,7 +1125,7 @@ module Make
begin match Plugin.if_sat (full_slice ()) with begin match Plugin.if_sat (full_slice ()) with
| Plugin_intf.Sat -> () | Plugin_intf.Sat -> ()
| Plugin_intf.Unsat (l, p) -> | Plugin_intf.Unsat (l, p) ->
let atoms = List.rev_map new_atom l in let atoms = List.rev_map create_atom l in
let c = make_clause (fresh_tname ()) atoms (Lemma p) in let c = make_clause (fresh_tname ()) atoms (Lemma p) in
Log.debugf info "Theory conflict clause: %a" (fun k -> k St.pp_clause c); Log.debugf info "Theory conflict clause: %a" (fun k -> k St.pp_clause c);
Stack.push c env.clauses_to_add Stack.push c env.clauses_to_add