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

debug

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 12:52:57 -04:00
parent 791290118b
commit 4eeec5487a
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -238,6 +238,13 @@ module Make(A : ARG)
(* then map subterms *) (* then map subterms *)
let t2 = Term.map_shallow self.tst aux t1 in (* map subterms *) let t2 = Term.map_shallow self.tst aux t1 in (* map subterms *)
let u = if t != t2 then aux t2 (* fixpoint *) else t2 in let u = if t != t2 then aux t2 (* fixpoint *) else t2 in
if t != u then (
Log.debugf 5
(fun k->k "(@[msat-solver.preprocess.term@ \
:from %a@ :to %a@])" Term.pp t Term.pp u);
);
Term.Tbl.add self.preprocess_cache t u; Term.Tbl.add self.preprocess_cache t u;
u u
(* try each function in [hooks] successively *) (* try each function in [hooks] successively *)
@ -246,16 +253,12 @@ module Make(A : ARG)
| h :: hooks_tl -> | h :: hooks_tl ->
match h self ~mk_lit ~add_clause t with match h self ~mk_lit ~add_clause t with
| None -> aux_rec t hooks_tl | None -> aux_rec t hooks_tl
| Some u -> | Some u -> aux u
Log.debugf 30
(fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])"
Term.pp t Term.pp u);
aux u
in in
let t = Lit.term lit |> simp_t self |> aux in let t = Lit.term lit |> simp_t self |> aux in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
Log.debugf 10 Log.debugf 10
(fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit'); (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
lit' lit'
let mk_lit self acts ?sign t : Lit.t = let mk_lit self acts ?sign t : Lit.t =