17988 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jakob Rath	7468b2326c	inequality	2022-11-28 18:00:17 +01:00
Jakob Rath	e6c9e13848	Disable copy/move of pdd_manager	2022-11-28 17:41:04 +01:00
Jakob Rath	77b4303b66	Don't jump over base level	2022-11-28 16:14:06 +01:00
Jakob Rath	1b1e310919	fix release build	2022-11-24 14:02:47 +01:00
Jakob Rath	3a92641ca0	Unit test: catch exceptions during instance setup	2022-11-23 17:02:15 +01:00
Jakob Rath	3713f51c15	Print unit test numbers	2022-11-23 17:01:11 +01:00
Jakob Rath	5c63a67634	disable for now	2022-11-23 16:59:26 +01:00
Jakob Rath	558fd718c0	Current base level may be too high to deallocate clause	2022-11-23 16:54:58 +01:00
Jakob Rath	0e32077321	Use insert_eval for potentially new constraints	2022-11-23 16:54:35 +01:00
Jakob Rath	76c106476c	superposition hotfix	2022-11-23 16:53:26 +01:00
Jakob Rath	bef1b9b429	Simplify	2022-11-23 15:11:27 +01:00
Jakob Rath	f51d5c2fe9	Add note on potential replay problem	2022-11-23 15:00:31 +01:00
Jakob Rath	0313f91dc2	fix	2022-11-23 14:55:41 +01:00
Jakob Rath	a39cce18cb	Fix another assertion	2022-11-23 13:46:44 +01:00
Jakob Rath	4224a14bdc	Need to re-check whether lemma was asserting	2022-11-23 13:22:43 +01:00
Jakob Rath	58c299dc33	fix assertion failure	2022-11-23 13:21:58 +01:00
Jakob Rath	2787a22007	Backtrack/backjump based on accumulated lemmas	2022-11-23 12:49:36 +01:00
Jakob Rath	fdc186b204	Simplify constraint evaluation	2022-11-23 12:19:03 +01:00
Jakob Rath	e4999b07aa	Remove active flag from constraint ... Superseded by boolean assignment and pwatch	2022-11-22 14:45:51 +01:00
Jakob Rath	da762700d6	quot_rem	2022-11-22 14:19:35 +01:00
Jakob Rath	85a633a3e0	Update resolve_value	2022-11-22 13:47:31 +01:00
Jakob Rath	a144a09ede	Propagation must be justified by a prefix of Gamma	2022-11-22 13:42:31 +01:00
Jakob Rath	33ea8d6e57	viable conflict also depends on vars	2022-11-22 13:40:29 +01:00
Jakob Rath	6e72a97727	Refactor assignment and search state	2022-11-21 17:25:15 +01: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
Jakob Rath	2c4e3184d7	For now, do not delete variables.	2022-11-16 15:49:58 +01: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
Jakob Rath	406696f0a3	Remove unused code	2022-11-11 10:25:49 +01:00
Jakob Rath	fc773ef19e	Remove old file	2022-11-10 14:42:55 +01:00
Jakob Rath	d3f70c0fb8	Rename: explain -> superposition	2022-11-10 14:42:13 +01:00
Nikolaj Bjorner	27f8b8d13a	inline definition in header file ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-09 09:55:05 -08:00
Nikolaj Bjorner	a98502b62f	weaken assertion, remove dependency on hash_compare in unittest for hashtables ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2022-11-09 09:28:49 -08:00
Jakob Rath	4b146a61ff	minor	2022-11-09 17:00:27 +01:00
Jakob Rath	abc4cc5295	Simplify boolean propagation level	2022-11-09 16:59:51 +01:00