23 commits

Author	SHA1	Message	Date
Simon Cruanes	721b1874b7	fix: re-check CC after calling on-final-check	2019-11-01 17:04:36 -05:00
Simon Cruanes	d4c3d3e443	cleanup: remove a few functions	2019-11-01 14:17:28 -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	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
Alexander Bentkamp	7fe6f07c0b	split on_merge into two events: pre and post 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	af0635dab7	fix: remove dead code	2019-06-10 16:04:01 -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	d1aec70cbe	fix: restore the module type coercion	2019-06-07 17:55:22 -05:00
Simon Cruanes	c9d8fd2f51	feat: ensure the congruence closure can propagate literals	2019-06-07 17:37:52 -05:00
Simon Cruanes	38f001b0e7	refactor: move Lit inside the solver, as output, not input	2019-06-07 17:31:11 -05:00
Simon Cruanes	ef1110925f	feat(cc): callback on propagations	2019-06-07 14:58:41 -05:00
Simon Cruanes	357dc73426	feat(check): use mini-cc to check CC conflicts on the fly	2019-06-07 14:47:52 -05:00
Simon Cruanes	2000114ab4	feat: add more stats	2019-06-07 13:27:03 -05:00
Simon Cruanes	e3e964a4c6	fix: first version that seems to work on QF_UF	2019-06-07 11:23:53 -05:00
Simon Cruanes	cad49b3747	wip: preprocess/simplify as part of theories	2019-06-06 17:13:21 -05:00
Simon Cruanes	2e7ab9ba9b	wip: simplify a lot and only keep th-bool-static in the functor	2019-06-05 16:53:13 -05:00
Simon Cruanes	080a20480f	refactor: continue functorization of sidekick	2019-05-27 19:55:21 -05:00
Simon Cruanes	6e9e95c233	wip: functorize everything	2019-05-26 23:20:47 -05:00