1739 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	8f577d3943	remove ast_manager get_sort method entirely	2021-02-02 13:57:01 -08:00
Nikolaj Bjorner	937b61fc88	fix build, refactor	2021-02-02 05:26:57 -08:00
Nikolaj Bjorner	3ae4c6e9de	refactor get_sort	2021-02-02 04:45:54 -08:00
Nikolaj Bjorner	4455f6caf8	move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail	2021-02-02 03:58:19 -08:00
Nikolaj Bjorner	6f346bf804	fix build break	2021-01-31 22:56:42 -08:00
Nikolaj Bjorner	33525007ab	try #4984 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-31 22:15:00 -08:00
Nikolaj Bjorner	20870c43ec	build test ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-31 20:49:53 -08:00
Nikolaj Bjorner	4dfdabc80f	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-31 16:36:55 -08:00
Nikolaj Bjorner	46f754c43d	add priority queue to instantiation	2021-01-31 16:17:52 -08:00
Nikolaj Bjorner	a1f46392aa	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-30 16:00:38 -08:00
Nikolaj Bjorner	657ed4db7a	fix relevancy bug for recfun ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-30 07:19:57 -08:00
Nikolaj Bjorner	ff475cbd5f	include rewriter_def	2021-01-29 17:17:22 -08:00
Nikolaj Bjorner	34c34b68ee	one more nightly ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-29 16:40:59 -08:00
Nikolaj Bjorner	4af9132f2e	more ematching	2021-01-29 13:39:14 -08:00
Nikolaj Bjorner	c0c314d1ae	build fix ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-29 06:23:27 -08:00
Nikolaj Bjorner	4e98a39d60	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-29 06:15:00 -08:00
Nikolaj Bjorner	f48fb8d3e8	it just works ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-28 11:12:05 -08:00
Nikolaj Bjorner	8a229bf684	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-27 22:39:02 -08:00
Nikolaj Bjorner	579caab025	na	2021-01-27 19:35:34 -08:00
Nikolaj Bjorner	4b6d7ca097	working on mam	2021-01-25 17:54:53 -08:00
Nikolaj Bjorner	680b185872	adding ematching engine, fixing seq_unicode	2021-01-22 17:10:45 -08:00
Nikolaj Bjorner	27ea23289e	fix #4955 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-20 00:30:11 -08:00
Nikolaj Bjorner	dc4382604b	fix #4955 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-20 00:29:09 -08:00
Nikolaj Bjorner	80033a5527	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-19 23:21:47 -08:00
Nikolaj Bjorner	95d98ea8ce	throttle equality propagation to shared expressions	2021-01-19 04:51:00 -08:00
Nikolaj Bjorner	7c34a54e8a	try different command-line ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-19 04:28:22 -08:00
Nikolaj Bjorner	64ba2a9fc9	fix gc of pb constraints ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-19 03:38:00 -08:00
Nikolaj Bjorner	01418a06a3	better staging of mbi based on generation	2021-01-18 16:55:58 -08:00
Nikolaj Bjorner	990aecceb7	change gc strategy for user-push/pop	2021-01-18 16:55:29 -08:00
Nikolaj Bjorner	b87405cc92	tune user-pop	2021-01-18 16:51:34 -08:00
Nikolaj Bjorner	91c54f6c39	na	2021-01-12 14:03:55 -08:00
Nikolaj Bjorner	d1dab327cd	fix build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-11 23:51:40 -08:00
Nikolaj Bjorner	0e429cab33	enable new core for incremental mode	2021-01-11 14:55:31 -08:00
Nikolaj Bjorner	bb56443e71	more #4932	2021-01-08 15:24:12 -08:00
Nikolaj Bjorner	e902e1ef13	fix #4931 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-01-08 12:02:53 -08:00
Nikolaj Bjorner	0173359a50	debugging/testing mbi	2021-01-07 17:32:05 -08:00
Nikolaj Bjorner	60ef60dff8	euf solver updates	2021-01-07 17:32:04 -08:00
Nikolaj Bjorner	523578e3f6	working on new solver core	2020-12-30 14:38:41 -08:00
Nikolaj Bjorner	374ae52d70	testing mbi	2020-12-26 13:49:59 -08:00
Nikolaj Bjorner	372e5ca569	fixes in new solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-12-25 11:19:31 -08:00
Nikolaj Bjorner	a164087384	remove cheap-eqs option as there is already propagate_eqs ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-12-21 11:04:04 -08:00
Nikolaj Bjorner	cd77a4d9a5	fix #4909 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-12-20 11:53:19 -08:00
Nikolaj Bjorner	11477f1ed1	fixes in new solver ... fix logging and lemma signs in arith_solver, move logging of drat equalities to euf	2020-12-16 10:40:17 -08:00
Nikolaj Bjorner	692bed7991	fix sign bug in internalization of literals	2020-12-14 17:33:14 -08:00
Nikolaj Bjorner	982da8db05	fix #4868	2020-12-07 10:27:00 -08:00
Nikolaj Bjorner	4d55f83654	misc	2020-12-04 16:59:13 -08:00
Nikolaj Bjorner	12198d13ac	fix #4794	2020-12-02 12:24:35 -08:00
Nikolaj Bjorner	9156e355d8	log	2020-11-30 11:57:25 -08:00
Nikolaj Bjorner	d6a5ef4343	add recfuns to Java #4820 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-11-25 12:25:20 -08:00
Nikolaj Bjorner	797f50e699	DRAT debugging updates	2020-11-22 15:38:57 -08:00