Commit Graph

22167 Commits

Author SHA1 Message Date
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
chriseth
6c2b686c0c Add header. 2022-03-20 20:19:19 +01:00