19391 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
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
Jakob Rath	6eb81fbb9d	use struct	2023-08-08 17:19:46 +02:00
Jakob Rath	3573305917	no need to keep an enode_pair, since the other is always the root	2023-08-08 17:13:05 +02:00
Jakob Rath	99a078dd69	add note on current example	2023-08-08 16:21:07 +02:00
Jakob Rath	5ec11c591f	slicing-conflict debug output	2023-08-08 16:05:36 +02:00
Jakob Rath	46a794ff67	slicing with fixed bits (wip)	2023-08-08 16:04:21 +02:00
Jakob Rath	f22ed9002f	tab -> space	2023-08-08 15:44:44 +02:00
Jakob Rath	63c41c3e04	Use struct fixed_bits_info instead of separate arguments ... and track sat::literal as justifications rather than viable::entry (we won't have a viable::entry for fixed bits coming from slicing)	2023-08-08 15:40:57 +02:00
Jakob Rath	e832325a8b	viable::entry::refined can be a boolean flag ... because we always copy the 'src' from the original entry to the refined one	2023-08-08 14:35:26 +02:00
Jakob Rath	036a3f31ca	call m_egraph.merge() at a single point	2023-08-07 17:56:43 +02:00
Jakob Rath	d36262d731	fix unit tests	2023-08-07 17:38:00 +02:00
Jakob Rath	4b4f0558b4	no need to introduce names for zero_ext/sign_ext arguments	2023-08-07 15:44:06 +02:00
Jakob Rath	5c53f588b7	Additional shortcuts for extract/concat	2023-08-07 15:33:51 +02:00
Jakob Rath	bc0119f333	Treat constraints of the form "x = val" more like variable assignments	2023-08-07 15:28:17 +02:00
Jakob Rath	aa81f6c9fb	Propagate value assignments discovered by the slicing e-graph	2023-08-07 15:20:04 +02:00
Jakob Rath	3fe591e5bb	Also print original exprs for polysat unsat core	2023-08-07 14:39:45 +02:00