cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
22,147 Commits 348 Branches 121 Tags
fullSMT
Commit Graph
22147 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
chriseth 3fdca88711 some tests 2022-04-27 15:40:35 +02:00
chriseth 591cb938bc some notes 2022-04-27 15:24:47 +02:00
chriseth 1a244e7a20 add comment 2022-04-17 19:30:03 +02:00
chriseth ecb90b69bd fix multi assignmnets 2022-04-17 18:30:15 +02:00
chriseth 9da8d7f28c Fix for implementation. 2022-04-17 18:20:35 +02:00
chriseth 1cc485bf72 use z3 2022-04-17 18:11:42 +02:00
chriseth 4ace0ed82c Correct test. 2022-04-17 18:11:30 +02:00
chriseth af1e8dba30 add note 2022-04-17 18:11:21 +02:00
chriseth 86fde5d357 ssa encoding 2022-04-17 17:54:39 +02:00
chriseth dc6eecd4ba Some tests. 2022-04-13 17:46:46 +02:00
chriseth c40c619daa Keep list of potentially violating variables. 2022-04-07 18:56:18 +02:00
chriseth f9ab7cc635 rewrite 2022-04-07 18:12:40 +02:00
chriseth aebe9753ff Some more work. 2022-04-02 15:46:43 +02:00
chriseth c3583a7b01 Cache simplex. 2022-04-01 21:19:56 +02:00
chriseth 5e904872bd Fix bounds. 2022-04-01 19:17:16 +02:00
chriseth 2ef255bdab Turn into class. 2022-04-01 19:03:21 +02:00
chriseth e2eeed6af1 Simplex with bounds. 2022-04-01 18:08:05 +02:00
chriseth 0592b6d86a Small opt in pivot. 2022-04-01 13:14:40 +02:00
chriseth 0b6e16983a Copy on write for fixed variables. 2022-03-24 01:45:46 +01:00
chriseth e4ad6ef39f Use unordered map. 2022-03-24 01:37:41 +01:00
chriseth 1b44668b34 Implement copy on write for sub problems. 2022-03-24 00:52:32 +01:00
chriseth b5aa534c43 Tiny tweak. 2022-03-24 00:31:52 +01:00
chriseth 65b1636867 Share ground state. 2022-03-24 00:27:54 +01:00
chriseth dd1092fda2 Re-add cache. 2022-03-24 00:08:28 +01:00
chriseth 5993cfa732 store variables per subproblem 2022-03-23 23:53:30 +01:00
chriseth 4235933124 simplify. 2022-03-23 23:13:57 +01:00
chriseth 7cfc2f6a12 Incremental lp solver. 2022-03-23 22:12:23 +01:00
chriseth 4171716e72 Add interface to make theory solver aware of decision levels. 2022-03-23 19:21:36 +01:00
chriseth 0c89ef6863 Different impl. 2022-03-23 18:58:45 +01:00
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