17912 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jakob Rath	ea9e5a47c7	-1	2022-11-30 15:24:35 +01:00
Jakob Rath	a8ecfd1313	unit test filter	2022-11-30 15:15:26 +01:00
Jakob Rath	7712068034	Remove old code ... backjump_and_learn, learn_lemma	2022-11-30 15:14:25 +01:00
Jakob Rath	fdca0cd86f	assign_verify: separate lemma production and activation	2022-11-30 15:00:58 +01:00
Jakob Rath	e338d42cff	Allow creation of op_constraint lemmas without adding them	2022-11-30 14:57:14 +01:00
Jakob Rath	5069796755	Create clauses without adding them	2022-11-30 14:51:43 +01:00
Jakob Rath	29180e7d0b	clause_builder::set_redundant	2022-11-30 14:50:53 +01:00
Jakob Rath	9b10733ebd	assignment helpers	2022-11-30 14:50:14 +01:00
Jakob Rath	54a21e764d	Remove old code ... backjump_lemma, revert_decision, revert_bool_decision	2022-11-30 12:21:39 +01:00
Jakob Rath	b4b94c954b	Try to produce an op_constraint lemma before invoking the fallback solver	2022-11-30 12:13:47 +01:00
Jakob Rath	2bc1b3a6dd	Better exception recording	2022-11-30 11:50:23 +01:00
Jakob Rath	ceddb97bfd	Disable asserts	2022-11-30 11:48:39 +01:00
Jakob Rath	032e7e0337	Remove not_op	2022-11-30 11:47:00 +01:00
Jakob Rath	7febcd47ec	Forgot univariate shl	2022-11-30 11:38:16 +01:00
Jakob Rath	4026ac9427	For r = p & q: "p = 0 => r = 0" is subsumed by "r <= p"	2022-11-30 11:35:36 +01:00
Jakob Rath	e6eea83b67	Missed some univariate constraints	2022-11-29 15:51:34 +01:00
Jakob Rath	5b6e383c88	Pretty-print powers of two	2022-11-29 15:49:58 +01:00
Jakob Rath	630276dbad	Re-enable saturation	2022-11-29 10:00:25 +01:00
Jakob Rath	4aa04fa475	Lemma names	2022-11-28 19:13:38 +01:00
Jakob Rath	0c44391b9e	Don't call assign_eh for internal constraints	2022-11-28 18:43:19 +01:00
Jakob Rath	c1f9a26f09	disable assertion for now	2022-11-28 18:15:24 +01:00
Jakob Rath	a3767b177c	comment	2022-11-28 18:11:51 +01:00
Jakob Rath	c488a766b5	Unit testing fixes	2022-11-28 18:05:25 +01:00
Jakob Rath	3d79cddf33	Update saturation inferences	2022-11-28 18:02:18 +01:00
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