22168 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
chriseth	874a8a4753	more code.	2022-03-23 17:36:02 +01:00
chriseth	e6f517fca1	delta	2022-03-23 14:54:31 +01:00
chriseth	72ae0f6a1a	Use enumerate.	2022-03-21 19:36:11 +01:00
Mate Soos	f163f9b7ce	Improving polarity caching to target phases	2022-03-21 18:59:48 +01:00
Mate Soos	a13b5332c2	Fixing minor last things	2022-03-21 18:26:25 +01:00
Mate Soos	a7a6475f6f	Fixing remaining issues	2022-03-21 18:04:01 +01:00
Mate Soos	3e0f4cd7bb	Adding example SAT solver	2022-03-21 17:52:47 +01:00
Mate Soos	09e3980b20	Adding VSIDS variable picking, restarts, and polarity caching	2022-03-21 17:46:40 +01:00
chriseth	dd777baabf	Fix mul implementation.	2022-03-21 16:11:10 +01:00
chriseth	0966c77fa6	Comment	2022-03-21 12:36:43 +01:00
chriseth	3996d5bad3	Comment	2022-03-21 12:36:35 +01:00
chriseth	9ae32ed395	fixup! Simplify tostring.	2022-03-21 11:38:12 +01:00
chriseth	24068116d9	Simplify conditions.	2022-03-21 11:24:54 +01:00
chriseth	afc56db6d5	Simplify tostring.	2022-03-21 11:23:48 +01:00
chriseth	9ec7cf88ec	Reasoning is always valid.	2022-03-21 10:54:38 +01:00
chriseth	c34019f136	Fix and and change some conditions.	2022-03-21 10:34:53 +01:00
chriseth	a3f999a13e	temp	2022-03-20 22:34:37 +01:00
chriseth	22aba74176	Simplify condition.	2022-03-20 22:34:22 +01:00
chriseth	6f7f60903e	Hacky for loop implementation.	2022-03-20 22:34:22 +01:00
chriseth	cfc6e02a28	Activate.	2022-03-20 22:34:22 +01:00
chriseth	d3aa06dc12	Fix opcodes.	2022-03-20 22:34:22 +01:00
chriseth	118a0f2125	slt test case.	2022-03-20 22:34:22 +01:00
chriseth	aa1e56bf2c	Fix slt	2022-03-20 22:34:22 +01:00
chriseth	1efa03201d	Fix ite	2022-03-20 22:34:22 +01:00
chriseth	2108580df6	Add equality constraints.	2022-03-20 22:34:22 +01:00
chriseth	33f0e0d4b2	Remove "only single constraint" restriction.	2022-03-20 22:34:22 +01:00
chriseth	fe15610ba4	some more debugging output	2022-03-20 22:34:22 +01:00
chriseth	c8c9067c9b	more code	2022-03-20 22:34:22 +01:00
chriseth	b4dd0420ca	encoding	2022-03-20 22:34:22 +01:00
chriseth	797651c74b	Typos.	2022-03-20 22:34:22 +01:00
chriseth	29be0d23f6	Enable magic squares 4	2022-03-20 22:34:22 +01:00
chriseth	b6e6cd4ebb	Compilation fix.	2022-03-20 22:34:22 +01:00
chriseth	6b7c200891	remove couts	2022-03-20 22:34:21 +01:00
chriseth	a3a0f1d95b	fixes	2022-03-20 22:33:47 +01:00
chriseth	3439776209	Combined solver.	2022-03-20 22:33:47 +01:00
chriseth	84c5c37c31	cdcl	2022-03-20 20:19:33 +01:00
chriseth	922837b44c	Forward unknown.	2022-03-20 20:19:20 +01:00
chriseth	3203b73c64	Some debug output.	2022-03-20 20:19:20 +01:00
chriseth	005e743fc5	Add fuzzer test case.	2022-03-20 20:19:20 +01:00
chriseth	a1ed2c0f09	Update libsolutil/LP.cpp ... Co-authored-by: Bhargava Shastry <bhargava.shastry@ethereum.org>	2022-03-20 20:19:20 +01:00
chriseth	f77f0ecae4	Update libsolutil/LP.h ... Co-authored-by: Bhargava Shastry <bhargava.shastry@ethereum.org>	2022-03-20 20:19:20 +01:00
chriseth	1e1964362c	Print reasons.	2022-03-20 20:19:20 +01:00
chriseth	8fbefb9c85	Tests for reason computation.	2022-03-20 20:19:20 +01:00
chriseth	337aea9483	Merge leftover.	2022-03-20 20:19:20 +01:00
chriseth	696515fe69	Add reasons.	2022-03-20 20:19:20 +01:00
chriseth	0a11aedc90	Extract problem splitter.	2022-03-20 20:19:20 +01:00
chriseth	88c63c3054	Apply suggestions from code review ... Co-authored-by: Bhargava Shastry <bhargava.shastry@ethereum.org>	2022-03-20 20:19:20 +01:00
chriseth	3c75adecc6	Add test.	2022-03-20 20:19:20 +01:00
chriseth	0e54562de4	Fix fuzzer bug.	2022-03-20 20:19:19 +01:00
chriseth	83b96e6a75	qualify move	2022-03-20 20:19:19 +01:00