832 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Simon Cruanes	591337855e	wip	2019-11-21 13:15:12 -06:00
Simon Cruanes	789f787df2	try on 4.05 for now	2019-11-21 13:09:56 -06:00
Simon Cruanes	9ef87a59e5	chore: try github actions	2019-11-21 13:06:14 -06:00
Simon Cruanes	61b5e9cee2	chore: simplify dune file	2019-11-19 16:22:49 -06:00
Simon Cruanes	0aa7a4ea25	chore: update test config	2019-11-19 16:16:47 -06:00
Simon Cruanes	801e3d25b4	chore: update travis	2019-11-07 10:37:00 -06:00
Simon Cruanes	409fe49ff0	feat(bin): use stmlib-utils 0.1, with versionned API and new statements	2019-11-07 10:35:59 -06:00
Simon Cruanes	239cff7445	chore: update travis	2019-11-05 17:12:11 -06:00
Simon Cruanes	8162a841fe	refactor: depend on smtlib-utils instead of having custom parser	2019-11-05 17:11:32 -06:00
Simon Cruanes	721b1874b7	fix: re-check CC after calling on-final-check	2019-11-01 17:04:36 -05:00
Simon Cruanes	3cd79ee4c9	refactor(th_bool): cache tseitin on absolute values	2019-11-01 15:53:12 -05:00
Simon Cruanes	b9965ca709	feat(th-cstor): reimplement the theory	2019-11-01 15:11:19 -05:00
Simon Cruanes	2d1d6ee937	feat: in main, --dot forces --check	2019-11-01 15:10:57 -05:00
Simon Cruanes	5b3cadf1e1	fix: missing type equality	2019-11-01 15:10:43 -05:00
Simon Cruanes	d4c3d3e443	cleanup: remove a few functions	2019-11-01 14:17:28 -05:00
Simon Cruanes	4875b07d0b	feat: add Ite constructor in base-term, handle it in mini-cc	2019-10-30 15:41:52 -05:00
Simon Cruanes	09ead7c41a	feat(mini-cc): add clear operation	2019-10-30 15:32:45 -05:00
Simon Cruanes	71db47f9ac	test: more CC tests	2019-10-30 15:03:24 -05:00
Simon Cruanes	c9f0141591	fix(mini-cc): handle not properly	2019-10-30 15:00:57 -05:00
Simon Cruanes	be2bc6e0f6	fix(term): missing type constraint	2019-10-30 15:00:49 -05:00
Simon Cruanes	1428d43369	test: add some unit tests for mini-cc	2019-10-30 15:00:34 -05:00
Simon Cruanes	17aba9461c	refactor(mini-cc): remove distinct API	2019-10-30 13:41:09 -05:00
Simon Cruanes	44e168495b	cleanup: remove dead code	2019-10-30 13:41:02 -05:00
Simon Cruanes	9ddce6a186	feat(check-cc): add statistics	2019-10-30 13:31:04 -05:00
Simon Cruanes	7d8589accd	refactor: change the functor stack	2019-10-29 15:06:19 -05:00
Simon Cruanes	94ba04a49e	wip: resume work on th-cstors	2019-10-29 14:32:31 -05:00
Simon Cruanes	4ab1997b45	chore: add 4.09 in travis	2019-10-29 14:32:24 -05:00
Simon Cruanes	0031c64ea9	feat(th-bool-static): check for new terms in the CC in final check	2019-10-08 09:08:05 -05:00
Simon Cruanes	d0b9c76629	Merge branch 'master' of github.com:c-cube/sidekick	2019-10-07 09:25:21 -05:00
Simon Cruanes	49a7446631	feat(th-bool-static): add non-traversable opaque boolean term	2019-10-05 18:37:49 -05:00
Simon Cruanes	1658887ea3	feat: basic production of models	2019-10-02 18:44:02 -05:00
Simon Cruanes	7552808c33	feat: add is_valid_literal filter to add_term_rec	2019-10-02 18:16:51 -05:00
Simon Cruanes	238226500a	feat: add is_valid_literal filter to add_term_rec	2019-10-02 18:15:06 -05:00
Alexander Bentkamp	7fe6f07c0b	split on_merge into two events: pre and post merge	2019-08-21 11:43:59 -05:00
Alexander Bentkamp	cde983df86	add assert for Expl.mk_merge	2019-08-21 11:43:59 -05:00
Simon Cruanes	769b80030a	feat: progress bar in solver	2019-07-31 04:36:32 -05:00
Simon Cruanes	d527b2b945	fix: remove some module aliases for 4.08	2019-07-31 03:25:04 -05:00
Simon Cruanes	2b40bd9db1	chore: add 4.08 to travis	2019-07-31 03:24:58 -05:00
Simon Cruanes	33a7843162	feat: expose more from atoms	2019-06-13 10:43:04 -05:00
Simon Cruanes	2430eb754d	feat(cc): make bitfields non-global; remove dead code	2019-06-11 11:38:54 -05:00
Simon Cruanes	ed4ba4057f	feat: solver actions are the same as CC actions	2019-06-11 10:28:00 -05:00
Simon Cruanes	3e7ef47fab	feat: add CC.merge_t	2019-06-11 10:26:04 -05:00
Simon Cruanes	1212e219eb	refactor: make backtrackable table polymorphic in values	2019-06-11 10:19:07 -05:00
Simon Cruanes	af0635dab7	fix: remove dead code	2019-06-10 16:04:01 -05:00
Simon Cruanes	36449d1645	feat(cc): expose a way to access bitfields	2019-06-10 15:19:57 -05:00
Simon Cruanes	ac99903aec	feat: add backtrackable table	2019-06-10 14:55:38 -05:00
Simon Cruanes	6c603d5589	refactor: remove code that checks invariants	2019-06-10 14:28:05 -05:00
Simon Cruanes	b2f6a30cc8	feat: function to add a theory and retain its state	2019-06-10 14:16:09 -05:00
Simon Cruanes	128e7dceb8	refactor: move Hash to util/; fix some warnings	2019-06-10 10:46:16 -05:00
Simon Cruanes	b8fd24ea7b	tool: update analyse.py with the minisat-ml version	2019-06-10 09:56:32 -05:00