7 commits

Author	SHA1	Message	Date
Simon Cruanes	5ca966a827	depth-restricted printing for terms and pterms	2022-10-13 21:43:16 -04:00
Simon Cruanes	fb8614f304	feat: decode proofs from traces; print them in show_trace	2022-10-13 00:03:08 -04:00
Simon Cruanes	48ebeb37fb	refactor(proof): serialize pterms; tracer inherits term tracer	2022-10-12 22:19:13 -04:00
Simon Cruanes	51c48453ab	wip: feat(proof): lib sidekick.proof with tracing	2022-10-12 12:17:35 -04:00
Simon Cruanes	af1ef089af	wip: proper proof production using Proof_ser-based traces	2021-10-15 23:00:09 -04:00
Simon Cruanes	bbb995b0d5	refactor some names related to proofs; wip add unit paramod	2021-10-03 20:32:37 -04:00
Simon Cruanes	9f01b98cde	wip: imperative proofs ... - getting closer to having the SMT solver compile again - dummy proof implementation - DRUP proof implementation for pure SAT solver	2021-08-18 23:59:39 -04:00