Commit Graph

22179 Commits

Author SHA1 Message Date
Mate Soos
3073def64d To remove compile issues 2022-07-01 23:13:29 +02:00
Mate Soos
6ca4979a2b No need for this change 2022-07-01 23:13:29 +02:00
Mate Soos
0193a3f315 Making things more solidity-like 2022-07-01 23:13:29 +02:00
Mate Soos
2d8adb7651 Adding required stuff for static compilation 2022-07-01 23:13:29 +02:00
chriseth
1e9206e01a Remove error output. 2022-07-01 14:11:30 +02:00
chriseth
bfc9c91539 Improved iteration. 2022-06-30 21:19:36 +02:00
chriseth
82604f8269 Variable names only for debug. 2022-06-29 11:19:10 +02:00
chriseth
eafe0e0621 Incremental parsing. 2022-06-29 10:53:13 +02:00
chriseth
7abe2750c6 Print success. 2022-06-27 17:52:13 +02:00
chriseth
cc3c2138a6 Avoid copying sorts. 2022-06-27 15:48:15 +02:00
chriseth
87bffbba98 Avoid copying let bindings. 2022-06-27 15:25:30 +02:00
chriseth
acfe18cd4e Ignore set-option. 2022-06-23 17:14:59 +02:00
chriseth
ae6f8e25b6 Some tweaks. 2022-06-23 16:03:36 +02:00
chriseth
0e0518e5ce Implement push and pop. 2022-06-23 15:18:34 +02:00
chriseth
4098661b89 Fix guessing of numbers. 2022-06-23 15:18:26 +02:00
chriseth
27261f6703 Remove hash functions. 2022-06-07 11:02:18 +02:00
chriseth
0e06440153 true/false literals. 2022-06-01 23:39:43 +02:00
chriseth
5c1ecce2a3 Implement inner xor. 2022-06-01 22:16:16 +02:00
chriseth
68bfbdb2a6 Support all fractional constants. 2022-06-01 22:03:58 +02:00
chriseth
cd3b7e333d Implement inner ite. 2022-06-01 16:59:09 +02:00
chriseth
9078ed8afd Implement => for boolean equality. 2022-06-01 13:23:43 +02:00
chriseth
57c6c529d0 Fix interior multi-or and multi-and. 2022-05-31 14:21:13 +02:00
chriseth
02c6298ab8 Cope with trailing whitespace. 2022-05-31 14:06:12 +02:00
chriseth
3cc853c2a0 Remove unused solving state. 2022-05-31 13:59:02 +02:00
chriseth
0f4cc05667 Copy-on-write let bindings. 2022-05-31 11:32:13 +02:00
chriseth
0a4f4f6f55 Improved reason computation. 2022-05-30 19:00:06 +02:00
chriseth
faa3a242ee Support some xor. 2022-05-30 18:17:16 +02:00
chriseth
973442c206 Parse let bindigns of literals speciall. 2022-05-30 18:11:40 +02:00
chriseth
e655f53813 Fix toString. 2022-05-30 11:08:51 +02:00
chriseth
62051ade2b Implement multi-argument addition. 2022-05-18 17:57:01 +02:00
chriseth
77d1ebae3b debugging output 2022-05-18 16:18:49 +02:00
chriseth
56d5f6d926 debugging 2022-05-16 19:14:31 +02:00
chriseth
657a02771b strict inequalities 2022-05-12 22:54:04 +02:00
chriseth
7b0e02b1ff mark rational encoding problems 2022-05-12 10:26:57 +02:00
chriseth
074969b5d9 implemert strict comparisons 2022-05-12 10:22:32 +02:00
chriseth
b76d3a6a0d some fixes and let bindings. 2022-05-12 09:49:08 +02:00
chriseth
33f952dc5f More solsmt. 2022-05-10 09:46:24 +02:00
chriseth
91f32a7beb Multi-argument and and or. 2022-05-10 08:58:41 +02:00
chriseth
f940e1f9e7 Disallow unknown operators. 2022-05-10 08:44:55 +02:00
chriseth
6bd09ba9d5 smt solver 2022-05-09 18:48:47 +02:00
chriseth
3e36c97367 Better assertions for boolean lp. 2022-05-09 17:22:38 +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