18875 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jakob Rath	0e20198473	should eval new constraints	2023-03-17 23:58:47 +01:00
Jakob Rath	931e6d655e	disable conflicts logging by default	2023-03-17 23:37:32 +01:00
Jakob Rath	a10a7e31a6	unused variable	2023-03-17 23:25:20 +01:00
Jakob Rath	317fed1062	assertion was too strong	2023-03-17 23:25:07 +01:00
Jakob Rath	526a55f116	Try to evaluate constraints whenever one of its variables is changed	2023-03-17 22:19:46 +01:00
Jakob Rath	f82f18efda	remove unused replay code	2023-03-17 21:12:26 +01:00
Jakob Rath	28716d1e67	Don't do complicated stuff in report_unsat, instead don't skip resolutions that we should not skip.	2023-03-17 21:09:52 +01:00
Jakob Rath	6bbfdb5289	restore intervals after backjump	2023-03-17 17:48:40 +01:00
Jakob Rath	d24c9352a4	fix assertion	2023-03-17 16:54:02 +01:00
Jakob Rath	89aaf4b1a6	resume conflict	2023-03-17 14:35:15 +01:00
Jakob Rath	cdd2dbcc41	combine different propagation functions	2023-03-17 13:25:22 +01:00
Jakob Rath	2000ab2cfc	report_unsat: propagate after backjump to restore conflict dependencies	2023-03-17 13:07:07 +01:00
Jakob Rath	6c9cf6182c	update comment	2023-03-16 16:55:40 +01:00
Jakob Rath	8493ebbaba	nicer conditions	2023-03-16 16:51:18 +01:00
Jakob Rath	a6771eb567	bool watch: order by search index instead of decision level	2023-03-16 16:50:09 +01:00
Jakob Rath	9af86f2d68	debug output	2023-03-16 16:13:13 +01:00
Jakob Rath	ce04d9c73b	Remove old bounds code for now	2023-03-16 13:23:37 +01:00
Nikolaj Bjorner	93360318b2	fixes to asserts ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-16 11:55:23 +01:00
Nikolaj Bjorner	1ba86c8ce3	fixup assertion ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-16 08:38:10 +01:00
Nikolaj Bjorner	622b8431b3	use v1, v2 instead of r1, r2 (roots) to get narrower equality conflicts ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-16 08:26:42 +01:00
Nikolaj Bjorner	c8e3ab75dc	fix unsoundness bug related to tracking equality assumptions outside of polysat ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-16 06:23:17 +01:00
Clemens Eisenhofer	eab31d5600	Moved logging to better place	2023-03-15 17:00:39 +01:00
Clemens Eisenhofer	135da9b824	Log also last conflict	2023-03-15 16:22:58 +01:00
Jakob Rath	03a6d74c58	fix eval justifications	2023-03-15 11:33:20 +01:00
Jakob Rath	5eb9fb2eb1	Check all bool/eval conflicts on the search stack before activate/narrow	2023-03-13 16:51:33 +01:00
Jakob Rath	47d6663c67	support other ops	2023-03-13 09:29:21 +01:00
Jakob Rath	3b7b7a6867	Fix parity lemma	2023-03-13 07:55:42 +01:00
Jakob Rath	69fbfc3616	fix	2023-03-13 07:37:17 +01:00
Jakob Rath	233baf170c	support checking pseudo-inverses	2023-03-12 18:31:57 +01:00
Jakob Rath	07d1f86575	cleanup conflict::init and promote assertion	2023-03-12 16:28:54 +01:00
Jakob Rath	aef0c739a7	Lemma validity check	2023-03-12 16:26:05 +01:00
Jakob Rath	50876a4dae	Add helper for printing polysat constraints	2023-03-12 16:15:25 +01:00
Jakob Rath	be72a37440	find_op_by_result_var	2023-03-12 16:14:12 +01:00
Jakob Rath	9a061d8f4a	find_op	2023-03-12 15:59:44 +01:00
Jakob Rath	9f7c9dfb17	fix one try_parity rule	2023-03-12 15:56:42 +01:00
Jakob Rath	f7baba4091	min_parity at most N	2023-03-11 23:23:32 +01:00
Jakob Rath	d4428c6cef	fix eval replay	2023-03-11 17:56:27 +01:00
Jakob Rath	3096ddaf33	disable old bounds prop as it is unsound	2023-03-11 11:22:24 +01:00
Jakob Rath	592b206097	fix lemma	2023-03-11 10:36:25 +01:00
Jakob Rath	f2ff1145bd	add some lemma names	2023-03-11 10:36:02 +01:00
Jakob Rath	d075759659	mk_clause with name	2023-03-11 10:32:19 +01:00
Jakob Rath	47f3353af6	Add int/unsigned overloads in pairs to avoid implicit conversions	2023-03-11 09:56:22 +01:00
Jakob Rath	1541c70b2b	Fix lemma_shl	2023-03-11 09:50:08 +01:00
Jakob Rath	ed03b5183e	do evaluation according to pvar watchlists	2023-03-10 15:52:24 +01:00
Jakob Rath	de88fb3875	revert	2023-03-10 15:36:30 +01:00
Jakob Rath	40d5b96ffa	Add assertion	2023-03-10 15:31:58 +01:00
Jakob Rath	c8c40f0154	Give higher priority to boolean propagation and bool/eval conflicts	2023-03-10 15:30:01 +01:00
Jakob Rath	538c4ee25f	hack to avoid wrong propagation justifications due to fallback solver	2023-03-10 12:42:00 +01:00
Jakob Rath	ffb7b5f85d	try_op bugfixes	2023-03-10 12:23:53 +01:00
Jakob Rath	dba8a4b73a	guard against different bitwidth	2023-03-09 13:51:10 +01:00