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

Debugging...

Browse source
This commit is contained in:
Guillaume Bury 2015-03-16 13:27:51 +01:00
parent 25dae83c6e
commit 31f5fdd1ae
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
solver/mcsolver.ml
View file

@ -612,10 +612,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
(* Propagation (boolean and theory) *) (* Propagation (boolean and theory) *)
let new_atom f = let new_atom f =
let a = add_atom f in L.debug 100 "New_atom";
L.debug 10 "New atom : %a" St.pp_atom a; let a = add_atom f in
ignore (th_eval a); L.debug 10 "New atom : %a" St.pp_atom a;
a ignore (th_eval a);
a
let slice_get i = Either.destruct (Vec.get env.trail i) let slice_get i = Either.destruct (Vec.get env.trail i)
(function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false) (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false)

4
solver/mcsolver_types.ml
View file

@ -172,9 +172,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
let add_term t = make_semantic_var t let add_term t = make_semantic_var t
let add_atom lit = let add_atom lit =
Log.debug 100 "entering add_atom"; L.debug 100 "entering add_atom";
let var, negated = make_boolean_var lit in let var, negated = make_boolean_var lit in
Log.debug 100 "found atom"; L.debug 100 "found atom";
if negated then var.tag.na else var.tag.pa if negated then var.tag.na else var.tag.pa
let make_clause name ali sz_ali is_learnt premise = let make_clause name ali sz_ali is_learnt premise =