16635 commits

Author	SHA1	Message	Date
Jakob Rath	c87aa8bcf8	fix slice_pp	2023-10-23 15:24:27 +02:00
Jakob Rath	482e4da4d7	skip on_merge for equality nodes	2023-10-23 15:24:02 +02:00
Jakob Rath	83aeba9ef4	fix	2023-10-23 11:46:43 +02:00
Jakob Rath	64ac3596bd	less nesting	2023-10-23 11:46:25 +02:00
Jakob Rath	38b0976adc	fix	2023-10-20 12:02:11 +02:00
Jakob Rath	a65c588a50	build_conflict_clause stub	2023-10-16 15:45:08 +02:00
Jakob Rath	816294025e	slicing minor	2023-10-16 15:33:43 +02:00
Jakob Rath	bb93a2ccb2	Avoid creating tautological clauses for quot_rem	2023-10-16 12:01:20 +02:00
Jakob Rath	e96f69e76c	Fix pdd_iterator for non-zero constant polynomials	2023-09-28 11:42:08 +02:00
Jakob Rath	3f0f70ba7c	Add missing return	2023-09-23 20:12:03 +02:00
Jakob Rath	4b29fbd4c7	Add missing include	2023-09-23 20:11:18 +02:00
Jakob Rath	66496c034f	prioritize decisions on variables of larger bit width	2023-09-06 10:52:47 +02:00
Jakob Rath	3687d69f2b	cp var_queue	2023-09-06 10:22:38 +02:00
Jakob Rath	d567d3b7f2	rename to try_congruence and add conditions	2023-08-18 17:11:46 +02:00
Jakob Rath	1316e1c881	fix splitting in merge	2023-08-18 17:03:49 +02:00
Jakob Rath	8a8afcdcb8	try_ugt_eq restores 6800	2023-08-18 16:24:06 +02:00
Jakob Rath	b4902f374b	slicing equivalent vars + explain	2023-08-18 16:21:59 +02:00
Jakob Rath	e09636065b	don't crash on null_literal	2023-08-18 15:30:39 +02:00
Jakob Rath	5bd35d764f	fix collect_fixed	2023-08-18 15:26:09 +02:00
Jakob Rath	efe0fa8e15	put add_var on the trail	2023-08-18 15:18:55 +02:00
Jakob Rath	1033c7e536	slicing replay was utterly broken	2023-08-18 15:10:23 +02:00
Jakob Rath	d3b5974448	shortcut in add_value ... otherwise, with literal x == a for constant a, we will create unnecessary value nodes. (because slicing will propagate x := a to the solver, which calls add_value in turn)	2023-08-18 15:00:00 +02:00
Jakob Rath	2d0120c621	Merge some intermediate slices ... In particular, this ensure propagates of values to extracted variables. (previously it could happen that x = y[h:l], y is assigned in the solver, but x is not propagated; because only base slices have been merged.)	2023-08-18 14:56:48 +02:00
Jakob Rath	49ca2d983d	remove abandoned code	2023-08-18 14:55:40 +02:00
Jakob Rath	cb14cb5743	(abandoned) attempt to propagate values upwards	2023-08-18 14:52:48 +02:00
Jakob Rath	9bffb34ce1	helpers	2023-08-18 14:47:29 +02:00
Jakob Rath	93592ea3f2	scoped_set_verbosity_level	2023-08-17 18:02:57 +02:00
Jakob Rath	dcb0d27dd7	Use get_bit instead of bitwise_and	2023-08-17 18:02:15 +02:00
Jakob Rath	19c1c7aa73	minor comments, skolem = false	2023-08-17 17:59:40 +02:00
Jakob Rath	3e7f7ef605	egraph comment, remove unneeded check	2023-08-17 17:57:42 +02:00
Jakob Rath	f8c9ed1d90	Revisit ule_constraint simplifications and add unit test for this ... If we can be certain of simplification results, it is easier to recognize patterns for fixed bits and similar.	2023-08-17 17:46:34 +02:00
Jakob Rath	6593754cd6	enable fixed bits in slicing	2023-08-17 17:37:11 +02:00
Jakob Rath	996012adb1	logging fix	2023-08-17 17:32:08 +02:00
Jakob Rath	0da1d9b218	display actual content of 'inequality' instances	2023-08-17 17:29:51 +02:00
Jakob Rath	9600f812a6	Functions to extract fixed bits for slicing	2023-08-17 17:26:19 +02:00
Jakob Rath	c95ff56d2d	slicing: change how values are tracked ... Do not eagerly merge equivalence classes with the same constant value. Reason: - when we split a value slice, the subslice might already exist in the egraph and already have subslices itself, which breaks assumptions in split/split_core. - introduces unnecessary splits Now: - wrap constants into fresh function symbol before creating the enode - check value compatibility in on_merge callback instead - track pointer to value_node for each enode, and update it in on_merge	2023-08-17 17:14:18 +02:00
Jakob Rath	08928d041a	explain_equal: jumping to root without explanation is wrong	2023-08-17 11:46:09 +02:00
Jakob Rath	53dc31989a	relax assertion	2023-08-17 09:32:47 +02:00
Jakob Rath	bc6f0729a0	Add lemma: y = x[h:l] & y != 0 ==> x >= 2^l	2023-08-16 09:58:56 +02:00
Jakob Rath	afc292e5db	Add parameter polysat.max_iterations for debugging	2023-08-16 09:55:21 +02:00
Jakob Rath	062ca92ebe	Switch between overflow representations with polysat.bvumulo=1/2	2023-08-16 09:54:04 +02:00
Jakob Rath	11b582cce7	Add rational::next_power_of_two	2023-08-16 09:48:32 +02:00
Jakob Rath	0bfebe3de1	Enable conflict logger with polysat.log_conflicts=true	2023-08-16 09:40:16 +02:00
Jakob Rath	20ab0bc13a	Invoke debugger if VERIFY fails in debug mode	2023-08-16 09:36:28 +02:00
Jakob Rath	1f640b96c9	compile unit tests	2023-08-14 14:00:41 +02:00
Jakob Rath	32d66951a8	bugfix	2023-08-11 14:52:26 +02:00
Jakob Rath	81609ed043	viable now takes into account fixed bits from slicing	2023-08-11 14:51:24 +02:00
Jakob Rath	586dcba661	slicing::collect_fixed should start at low-order base slice	2023-08-11 14:49:17 +02:00
Jakob Rath	89f0fb05a5	forgot to commit CMakeLists	2023-08-08 17:54:33 +02:00
Jakob Rath	f9cbee3b3d	explain_fixed is currently just explain_value for a slice	2023-08-08 17:26:52 +02:00