16568 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	b9f34286a7	generalize macro head detection and elaboration	2022-11-20 11:36:45 +07:00
Nikolaj Bjorner	fcaa85d7a8	#6456 - elaborate on error message	2022-11-20 11:27:39 +07:00
Nikolaj Bjorner	86f3702403	prevent re-declaration of enumeration sort names ... preventing redeclaration of all ADT cases is not part of this update.	2022-11-19 19:46:34 +07:00
Nikolaj Bjorner	c3c45f495a	add some comments to elim_predicates	2022-11-19 19:45:25 +07:00
Nikolaj Bjorner	251d49d133	remove outdated comment	2022-11-19 18:55:30 +07:00
Nikolaj Bjorner	3f10933225	remove VERBOSE 0	2022-11-19 18:55:01 +07:00
Nikolaj Bjorner	771157696b	new simplifier/tactic ... eliminate_predicates finds macros and eliminates predicates from formulas as pre-processing.	2022-11-19 18:51:20 +07:00
Nikolaj Bjorner	d735faae4e	add isolated hide/add model converter functions	2022-11-19 18:50:37 +07:00
Nikolaj Bjorner	a81a5ec68c	add virtual function requirement to dependent_expr_state	2022-11-19 18:46:31 +07:00
Nikolaj Bjorner	dcc995f0e5	code simplification	2022-11-19 18:45:54 +07:00
Nikolaj Bjorner	41b40c3a51	remove dead code	2022-11-19 18:45:07 +07:00
Nikolaj Bjorner	c2e9016d04	display model-add parameters in correct order	2022-11-19 18:44:52 +07:00
Nikolaj Bjorner	ba68652c72	add destructive equality resolution to existentials	2022-11-19 18:43:46 +07:00
Nikolaj Bjorner	7da91f4313	allow printing declarations with reverse variable order	2022-11-19 18:43:21 +07:00
Jakob Rath	022c06f75d	pdd::subst_get	2022-11-18 15:14:38 +01:00
Jakob Rath	adc9f7abe4	Add basic implementation of left shift	2022-11-17 17:37:52 +01:00
Jakob Rath	68707eefe7	Fix lshr axioms	2022-11-17 17:37:52 +01:00
Jakob Rath	80a2ac64de	Remove tst_polysat_argv	2022-11-17 17:37:52 +01:00
Jakob Rath	81150f433a	test	2022-11-17 17:37:52 +01:00
Jakob Rath	d9cb06114e	Print partial test results table on interrupt	2022-11-17 17:37:52 +01:00
Jakob Rath	f12ae0af12	clause_builder: rename push to insert	2022-11-17 17:37:52 +01:00
Jakob Rath	dbe814d568	Add forbidden interval lemma separately	2022-11-17 15:00:16 +01:00
Jakob Rath	b4ee8cef1a	Add helper for creating op_constraints	2022-11-17 12:59:37 +01:00
Jakob Rath	38a43bd087	Remove conflict_kind	2022-11-17 12:25:28 +01:00
Jakob Rath	00e8c53f9a	Remove unused code	2022-11-17 12:22:40 +01:00
Jakob Rath	097454cf37	Fix eval_lshr	2022-11-17 11:47:12 +01:00
Nikolaj Bjorner	59b7845c7d	reset visited (fast mark) to not clash with occurs	2022-11-17 17:36:21 +09:00
Nikolaj Bjorner	6662afdd26	perf improvements to solve-eqs and euf-completion	2022-11-16 22:15:02 -08:00
Jakob Rath	2c4e3184d7	For now, do not delete variables.	2022-11-16 15:49:58 +01:00
Nikolaj Bjorner	2c7799939e	wip - tuning and fixes to euf-completion	2022-11-16 03:47:38 -08:00
Nikolaj Bjorner	98fc8c99db	add shortcut to equality mk utility	2022-11-16 03:47:01 -08:00
Nikolaj Bjorner	55ab7778f4	fix perf bug in new solve_eqs.	2022-11-16 03:46:17 -08:00
Nikolaj Bjorner	d70dbdad50	wip euf-completion - debugging	2022-11-15 20:17:39 -08:00
Nikolaj Bjorner	255414f4a9	fix regression crash ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-15 11:20:12 -08:00
Nikolaj Bjorner	9845c33236	add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic	2022-11-15 09:13:13 -08:00
Nikolaj Bjorner	bfae8b2162	set flat_and_or to false in bv rewriter	2022-11-15 05:47:28 -08:00
Nikolaj Bjorner	041b5f9ef0	rename away solve_eqs2 to solve_eqs ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-14 20:01:37 -08:00
Nikolaj Bjorner	48c0f8694f	euf-completion bug fix, streamline name to solve_eqs	2022-11-14 20:01:00 -08:00
Nikolaj Bjorner	3eeb59db34	fix #6451 missing occurrence marking when there is an unsafe equality already ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-14 19:23:27 -08:00
Nikolaj Bjorner	95e07ffe8e	disable unsound context equality solving ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-14 19:14:51 -08:00
Nikolaj Bjorner	6297c001ee	remove legacy solve_eqs_tactic entirely ... also, bug fixes to elim_unconstrained (elim_uncnstr2) which is to replace legacy tactic for eliminating unconstrained constants.	2022-11-14 18:57:16 -08:00
Nikolaj Bjorner	3f2bbe5589	harness del_object #6452 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-14 08:54:08 -08:00
Jakob Rath	aa59de9056	Track max jump level from side lemmas	2022-11-14 15:43:46 +01:00
Jakob Rath	cd83a6ec69	Remove bailout state from conflict	2022-11-14 15:15:35 +01:00
Jakob Rath	e2804c3db2	Remove bail_vars	2022-11-14 15:02:58 +01:00
Jakob Rath	eec8e8ebe4	Fix name: value propagation -> evaluation (for boolean literals)	2022-11-14 14:58:20 +01:00
Jakob Rath	436881c18c	print lemmas	2022-11-14 14:51:54 +01:00
Jakob Rath	01af25ca02	Remove backjump state from conflict	2022-11-14 14:33:19 +01:00
Nikolaj Bjorner	3d2bf13577	streamline statistics, fix bug in updating goals	2022-11-13 20:30:00 -08:00
Nikolaj Bjorner	ce6cfeaa68	fix bug in euf-completion relating to missed normalization	2022-11-13 18:01:17 -08:00