28 commits

Author	SHA1	Message	Date
Simon Cruanes	f7195bf980	feat(smt): ability for a theory to declare we're in incomplete fragment	2022-01-11 14:00:04 -05:00
Simon Cruanes	af8ab338e6	feat(smt): add a registry to share values between theories	2022-01-11 14:00:04 -05:00
Simon Cruanes	63f50d03fa	feat: proper proof production for theory merges in CC ... this involves resolution steps between the lemma (typically a kind of horn clause with the merge as conclusion) and a bunch of literals responsible for some equational hypotheses of this horn clause, being true	2021-12-29 15:56:54 -05:00
Simon Cruanes	584b56075f	feat: add push/pop for assumptions; add check_sat_propagation_only ... this gives the user the possibility of controlling search by mostly using assumptions (and the underlying assumption stack) as well as boolean+theory propagation. The result is **not** complete, but can still help as a beefed-up contextual simplifier.	2021-12-20 15:34:34 -05:00
Simon Cruanes	5d2f8a1d3d	feat(api): add callbacks to measure progress or ask solver to stop	2021-12-20 13:51:59 -05:00
Simon Cruanes	c03fc97f00	better debug in CC	2021-12-17 16:41:00 -05:00
Simon Cruanes	b19d80e443	debug	2021-12-17 16:40:59 -05:00
Simon Cruanes	3ab1ddfea8	fix: ensure all functions in SMT solver preprocess their literals	2021-12-16 13:49:43 -05:00
Simon Cruanes	0abe4b7020	wip: decode more proof steps to quip	2021-10-27 21:50:28 -04:00
Simon Cruanes	3589592296	wip: use real proofs	2021-10-16 22:00:29 -04:00
Simon Cruanes	fd1d068997	proof stubs and sat proof	2021-10-12 22:13:28 -04:00
Simon Cruanes	4308eba04d	fix	2021-10-11 23:19:40 -04:00
Simon Cruanes	1779b7115a	wip: proof production (incl. better tracking of proofs in CC)	2021-10-11 14:27:14 -04:00
Simon Cruanes	0550f6fcfa	wip: proof production	2021-10-09 00:51:15 -04:00
Simon Cruanes	d3537f2c3f	wip: refactor proof	2021-10-07 20:49:39 -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	16bb65ebfa	wip: clause pools	2021-08-31 09:30:28 -04:00
Simon Cruanes	81caf4824e	wip: feat: additional clause allocators in SAT	2021-08-30 09:03:37 -04:00
Simon Cruanes	e7e8873295	fix more warnings	2021-08-27 09:28:59 -04:00
Simon Cruanes	5505ece5fb	chore: fix warning	2021-08-23 10:49:12 -04:00
Simon Cruanes	baecce0946	feat: use Stat in SAT solver	2021-08-22 01:56:54 -04:00
Simon Cruanes	27796da5a8	fix preprocessing in th-bool	2021-08-22 01:29:01 -04:00
Simon Cruanes	e93e084eac	refactor: eager proofs; stronger preprocessing ... proofs are now directly emitted (almost) everywhere, which simplifies a lot of things. preprocessing is more recursive (a bit too much really).	2021-08-22 01:13:41 -04:00
Simon Cruanes	0668f28ac7	try to fix boolean terms not decided by SAT solver	2021-08-21 14:00:31 -04:00
Simon Cruanes	1ab7d34a7d	refactor: make it compile again	2021-08-20 18:18:30 -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
Simon Cruanes	2bb6c94925	remove dead code	2021-08-18 00:01:54 -04:00
Simon Cruanes	10a4cf4c29	refactor: rename sidekick-msat-solver into sidekick-smt-solver	2021-08-18 00:01:25 -04:00