173 Commits

Author	SHA1	Message	Date
chriseth	14284ef1b1	Implement LinearExpression using a sparse vector.	2022-03-22 13:39:37 +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	09e3980b20	Adding VSIDS variable picking, restarts, and polarity caching	2022-03-21 17:46:40 +01:00
chriseth	9ae32ed395	fixup! Simplify tostring.	2022-03-21 11:38:12 +01:00
chriseth	afc56db6d5	Simplify tostring.	2022-03-21 11:23:48 +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	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	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	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	0e54562de4	Fix fuzzer bug.	2022-03-20 20:19:19 +01:00
chriseth	83b96e6a75	qualify move	2022-03-20 20:19:19 +01:00
chriseth	6c2b686c0c	Add header.	2022-03-20 20:19:19 +01:00
chriseth	0f705c8a82	Cache solution for the case where we are not interested in models.	2022-03-20 20:19:19 +01:00
chriseth	8835b95719	comment	2022-03-20 20:19:19 +01:00
chriseth	592b421f44	Extract problem splitter.	2022-03-20 20:19:19 +01:00
chriseth	db9028906a	small optimization.	2022-03-20 20:19:19 +01:00
chriseth	5faebbff39	Extract simplification class.	2022-03-20 20:19:19 +01:00
chriseth	dec67df8d8	Refactor.	2022-03-20 20:19:19 +01:00
chriseth	6bff7a1e91	cleanup	2022-03-20 20:19:19 +01:00
chriseth	cf6cf5bba2	cleanup	2022-03-20 20:19:19 +01:00
chriseth	8600760f3d	Cleanup	2022-03-20 20:19:19 +01:00
chriseth	f25cd708ea	Cleanup	2022-03-20 20:19:19 +01:00
chriseth	b1fcf023f9	Cleanup	2022-03-20 20:19:19 +01:00
chriseth	00a277c0f5	Simplifications on LinearExpression.	2022-03-20 20:19:19 +01:00
chriseth	e6c67924b0	Fix compiler warning.	2022-03-20 20:19:18 +01:00
chriseth	7a250fea42	Use names for the bounds.	2022-03-20 20:19:18 +01:00
chriseth	751f50b6c3	LP Solver.	2022-03-20 20:19:18 +01:00