1887 commits

This branch

This branch

All branches

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	4e1272d64a	test: update doc guide	2022-10-12 22:45:47 -04:00
Simon Cruanes	032be221a3	refactor: fix sudoku example	2022-10-12 22:20:43 -04:00
Simon Cruanes	a6d3ed259f	refactor: make it compile again (driver, main)	2022-10-12 22:19:41 -04:00
Simon Cruanes	48ebeb37fb	refactor(proof): serialize pterms; tracer inherits term tracer	2022-10-12 22:19:13 -04:00
Simon Cruanes	ad0165242f	refactor: update remaining theories for new proof style	2022-10-12 22:19:00 -04:00
Simon Cruanes	f275129967	refactor(smt): use sidekick.proof for proof tracing	2022-10-12 16:30:39 -04:00
Simon Cruanes	6f576e7d8b	adapt bin	2022-10-12 15:51:37 -04:00
Simon Cruanes	85ba423e8c	wip: refactor(smt): use sidekick.proof for proof tracing	2022-10-12 12:22:19 -04:00
Simon Cruanes	46c44648e1	feat(core-logic): add builtin Proof type ... not used yet	2022-10-12 12:22:04 -04:00
Simon Cruanes	7db5e1a902	refactor(sat): use new proof tracer from sidekick,proof	2022-10-12 12:21:45 -04:00
Simon Cruanes	5135d9920a	refactor(asolver): use new proof tracer from sidekick.proof	2022-10-12 12:21:20 -04:00
Simon Cruanes	ef3f2713dc	refactor(cc): use new proof trace from sidekick.proof	2022-10-12 12:21:06 -04:00
Simon Cruanes	8a3e7528c3	refactor(simplify): use new proof trace from sidekick.proof	2022-10-12 12:20:50 -04:00
Simon Cruanes	4b359a40f2	improve Int_id for tracing	2022-10-12 12:20:20 -04:00
Simon Cruanes	2726a3afe2	refactor: remove proof-trace infra from base to use sidekick.trace instead	2022-10-12 12:20:04 -04:00
Simon Cruanes	842a7de435	wip: refactor(core): remove proof representation from core	2022-10-12 12:18:52 -04:00
Simon Cruanes	82727cd7ad	wip: feat(core): term references	2022-10-12 12:18:40 -04:00
Simon Cruanes	51c48453ab	wip: feat(proof): lib sidekick.proof with tracing	2022-10-12 12:17:35 -04:00
Simon Cruanes	ccd506e387	test	2022-10-10 20:15:18 -04:00
Simon Cruanes	89c9e00500	chore: fix opam file	2022-10-10 16:06:02 -04:00
Simon Cruanes	b577389acf	test	2022-10-10 15:45:53 -04:00
Simon Cruanes	a47bbf45e8	refactor: use abstract-solver in smtlib driver; CDCL(T) implements asolver ... this way we can add new SMT techniques without changing (much) the driver.	2022-10-10 15:44:13 -04:00
Simon Cruanes	d08c8fe165	feat: add sidekick.abstract solver ... this library provides an abstract interface for what a SMT solver provides, independently of the underlying implementation technology.	2022-10-10 15:43:37 -04:00
Simon Cruanes	e3e71f3d76	refactor: smtlib driver now part of base; make it stateful	2022-10-10 14:28:43 -04:00
Simon Cruanes	2f96f36e75	chore: generate opam files from dune-package	2022-10-10 13:41:07 -04:00
Simon Cruanes	4cb3299804	chore: ocamlformat	2022-10-05 09:16:32 -04:00
Simon Cruanes	656d93d5fb	smt tracer is now a clause tracer	2022-10-02 23:23:34 -04:00
Simon Cruanes	06a0089a8c	feat: add Clause_tracer, works both for SMT and SAT	2022-10-02 23:07:53 -04:00
Simon Cruanes	d9b76814dd	ignore	2022-10-02 23:07:45 -04:00
Simon Cruanes	96dddb5383	feat: show_trace, and trace_reader, can now display a QF_UF trace ... the trace can contain assertions.	2022-09-30 23:05:00 -04:00
Simon Cruanes	3aadc640c4	improve tracing, add show_trace	2022-09-30 22:11:41 -04:00
Simon Cruanes	8f563c838f	wip: Tracer for SMT	2022-09-26 22:44:43 -04:00
Simon Cruanes	342bf87759	refactor(core/term): tracer is now a class ... this way we can inherit it in tracers that can trace many things, including terms.	2022-09-26 22:43:49 -04:00
Simon Cruanes	40e124931c	doc: update readme	2022-09-26 21:00:09 -04:00
Simon Cruanes	1c11a82a7d	test: update doc guide	2022-09-26 20:57:55 -04:00
Simon Cruanes	dbe64f5975	feat: decoders for LRA terms	2022-09-26 20:57:48 -04:00
Simon Cruanes	17ac25d314	update tracing test	2022-09-26 20:47:48 -04:00
Simon Cruanes	45eebaae0f	some todos	2022-09-26 20:31:57 -04:00
Simon Cruanes	59306d2e01	fix sudoku solve	2022-09-26 20:14:26 -04:00
Simon Cruanes	a99fbed159	test: repair test	2022-09-25 23:13:45 -04:00
Simon Cruanes	8cbb200f18	basic test for tracer/trace reader using bencode	2022-09-25 23:05:16 -04:00
Simon Cruanes	c2e5f31645	change signature of Const.decoders; add bencode decoder	2022-09-25 23:05:15 -04:00
Simon Cruanes	9ea8ba9bd1	feat: implement some const decoders	2022-09-25 23:05:15 -04:00
Simon Cruanes	798993fee2	feat(trace): start basic trace reader for terms, using Source	2022-09-25 23:05:15 -04:00
Simon Cruanes	f2471fd78c	feat(trace): add Source, to read traces	2022-09-25 23:05:14 -04:00
Simon Cruanes	ca3262eac3	minor change in term tracer	2022-09-25 23:05:14 -04:00
Simon Cruanes	27b0374c62	feat(util): more functions in Ser_decode	2022-09-25 23:05:13 -04:00
Simon Cruanes	15bc5c4b60	feat(core): add LRU to support entry decoding in term reader	2022-09-25 23:05:13 -04:00