19379 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jakob Rath	df82d9b0f9	unsat core dbg	2023-03-23 13:53:13 +01:00
Jakob Rath	f364ba8c8a	remove unused code	2023-03-23 13:40:19 +01:00
Jakob Rath	50814c952a	nicer output	2023-03-23 13:39:01 +01:00
Jakob Rath	f0ac81a149	remove output (related bug has been fixed)	2023-03-23 09:53:47 +01:00
Jakob Rath	095dfb2115	minor, debug output	2023-03-23 09:49:00 +01:00
Jakob Rath	d2397deb8d	propagate before push	2023-03-23 09:35:10 +01:00
Jakob Rath	51025a75b4	fix conflict reset condition	2023-03-23 09:29:59 +01:00
Jakob Rath	4e9db7c4d9	eval justifications are determined by chronological order	2023-03-23 09:25:46 +01:00
Jakob Rath	5b3f500900	Try to keep conflict alive for longer	2023-03-23 07:18:36 +01:00
Jakob Rath	e433951e27	Active lemmas need to be queued for repropagation after resetting conflict	2023-03-22 17:44:02 +01:00
Nikolaj Bjorner	50bd6efea4	fix #6624	2023-03-22 14:00:09 +01:00
Nikolaj Bjorner	03a44803b6	fix #6635	2023-03-22 13:38:02 +01:00
Jakob Rath	2804453039	resolve_conflict should stop at base index	2023-03-22 12:43:39 +01:00
Nikolaj Bjorner	2683a2d6ed	fix #6637	2023-03-22 08:49:33 +01:00
Nikolaj Bjorner	53ca65a62e	fix unsound rewrite	2023-03-20 18:55:40 +01:00
Nikolaj Bjorner	f075dc2882	remove experimental files	2023-03-20 17:07:48 +01:00
Nikolaj Bjorner	48de7c2da8	missing updates	2023-03-20 17:07:04 +01:00
Nikolaj Bjorner	c6e3fb446a	print lemmas2console faster ... - add option pp.no_lets (default = false) to print formulas without let (used by the low-level SMT2 printer). - print lemmas2console faster by using the low level printer	2023-03-20 17:07:04 +01:00
Nikolaj Bjorner	a9e6e567b0	make generation of "some" Boolean value fair	2023-03-20 17:07:04 +01:00
Nikolaj Bjorner	d1c7ff1a36	add unconstrained elimination for sequences	2023-03-20 17:07:04 +01:00
Nikolaj Bjorner	da782a9dc7	remove references to linear propagate ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-20 09:20:00 +01:00
Nikolaj Bjorner	3dbca1042c	review comments ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-03-20 09:12:07 +01:00
Jakob Rath	7e6571309e	fix	2023-03-18 14:02:22 +01:00
Jakob Rath	707a5b78f7	Print less output in non-verbose mode	2023-03-18 08:04:03 +01:00
Jakob Rath	ee64bf27d1	correct version of reverted commit	2023-03-18 07:58:55 +01:00
Jakob Rath	a8315e8558	Revert "remove unused/broken code" ... This reverts commit b75fcb5714.	2023-03-18 07:57:27 +01:00
Jakob Rath	142e33d2f4	The justifications of value propagations may contain undiscovered bool/eval conflicts	2023-03-18 07:52:52 +01:00
Jakob Rath	b75fcb5714	remove unused/broken code	2023-03-18 07:51:20 +01:00
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