69 commits

Author	SHA1	Message	Date
Jakob Rath	bef1be8cb5	should not happen anymore	2022-10-07 10:11:00 +02:00
Jakob Rath	f184545aca	Debug dlist insertion ... Found because of assertion failure in test_polysat::test_fixed_point_arith_div_mul_inverse()	2022-10-05 17:24:28 +02:00
Jakob Rath	dc9373dcbd	Change old solver::propagate method	2022-10-04 17:09:09 +02:00
Jakob Rath	811843cf45	Fix interval check	2022-10-03 15:35:07 +02:00
Jakob Rath	6caa3ba1b7	Skip redundant intervals in viable::resolve (disabled for now)	2022-10-03 11:03:05 +02:00
Jakob Rath	3c60c418e7	fix assertion	2022-09-23 16:15:38 +02:00
Jakob Rath	6abe0c9be8	set, lemma, minor	2022-09-21 16:29:36 +02:00
Jakob Rath	b43971bb4a	Connect conflict2	2022-09-21 12:14:44 +02:00
Nikolaj Bjorner	48d5a98edc	meeting notes ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-09-19 09:10:11 -07:00
Jakob Rath	a416e16566	conflict2	2022-09-19 16:01:45 +02:00
Jakob Rath	c1e2ea80f5	make explicit that we compare the concrete values	2022-08-22 14:17:47 +02:00
Jakob Rath	a76f977f85	Change univariate fallback solver to one-shot mode for now	2022-08-02 12:42:34 +02:00
Jakob Rath	0fb8c72f50	print more information	2022-06-29 14:26:25 +02:00
Jakob Rath	be488f75ab	Add some fi info	2022-04-13 09:34:59 +02:00
Jakob Rath	9fa5096776	conflict logging	2022-04-12 16:06:20 +02:00
Jakob Rath	d41d3fa6ea	fix some bugs	2022-03-18 16:05:51 +01:00
Jakob Rath	fd353bff17	unsat core	2022-03-18 15:49:44 +01:00
Jakob Rath	509a007ed7	Integrate univariate solver in polysat	2022-03-18 15:43:06 +01:00
Jakob Rath	c648b57493	forbidden intervals only used by viable	2022-03-10 16:12:13 +01:00
Jakob Rath	22411f8b43	one more special case	2022-03-10 10:32:23 +01:00
Nikolaj Bjorner	8c9835bca6	smul no overflow ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-02-16 18:55:07 +02:00
Nikolaj Bjorner	4c4f916917	merge ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-02-02 08:24:58 -08:00
Nikolaj Bjorner	32edbfa28e	two bugs: check for always false, adjust start of list was incorrect during re-insert	2022-02-02 07:37:35 -08:00
Nikolaj Bjorner	18291543d6	fixing corner cases for viable intervals	2022-02-01 13:21:51 -08:00
Nikolaj Bjorner	c48f14e537	updated conflict state ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-02-01 11:47:33 -08:00
Jakob Rath	15854301b2	Generalize refine_disequal_lin	2022-01-31 15:35:25 +01:00
Nikolaj Bjorner	b488a1fadd	WIP revamp conflict state ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-01-29 16:17:58 -08:00
Nikolaj Bjorner	bbddeffe0b	check for 0 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-01-25 15:07:05 +01:00
Jakob Rath	8c2f268506	fi disequal: add special treatment for v > -a*v	2022-01-24 17:03:49 +01:00
Jakob Rath	fa75a9109e	Test forbidden intervals, disequal case	2022-01-19 19:06:35 +01:00
Jakob Rath	5886a8873c	forgot ceil	2021-12-24 06:57:40 +01:00
Jakob Rath	28864e563c	First version of refine_disequal_lin	2021-12-23 18:36:27 +01:00
Nikolaj Bjorner	8c2735e68b	prepare for diseq_lin viable	2021-12-13 12:00:19 -08:00
Nikolaj Bjorner	651b41f8c0	refactor fi functionality	2021-12-13 11:39:15 -08:00
Nikolaj Bjorner	ca3251b152	add widening in all cases	2021-12-13 10:55:03 -08:00
Nikolaj Bjorner	c7da31a67d	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-13 10:24:42 -08:00
Nikolaj Bjorner	d80b375ac3	accelerate	2021-12-12 14:33:57 -08:00
Nikolaj Bjorner	7bf76dd1f6	finally! ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-12 10:26:54 -08:00
Nikolaj Bjorner	83efb1413a	na	2021-12-11 08:41:04 -08:00
Nikolaj Bjorner	a4fc63c542	initial overflow test ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-09 14:39:00 -08:00
Nikolaj Bjorner	d7f16d0622	merge ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-09 08:26:34 -08:00
Nikolaj Bjorner	f3ac879fa4	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-09 08:25:52 -08:00
Nikolaj Bjorner	ca9fbcf6f4	merge ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-08 12:44:55 -08:00
Nikolaj Bjorner	8d3c3ede39	save ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-08 12:40:44 -08:00
Nikolaj Bjorner	4d0f55febd	update viable ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-12-03 17:57:08 -08:00
Nikolaj Bjorner	a81a00a93c	add support for non-unit coefficients ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-11-30 09:53:09 -08:00
Nikolaj Bjorner	7b85afbe9c	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-11-26 18:27:44 +01:00
Nikolaj Bjorner	fc6e127cca	don't add viable premises on decisions ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-11-25 20:19:58 +01:00
Nikolaj Bjorner	a4e29ecd7e	interval ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-11-25 18:46:43 +01:00
Nikolaj Bjorner	adf41c5d02	another bug fix ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-11-24 13:37:15 +01:00