Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding switch 'pdr -o' to control using property output in induction. | Alan Mishchenko | 2016-05-25 | 4 | -2/+10 |
| | |||||
* | Improving SMT-LIB parser. | Alan Mishchenko | 2016-05-23 | 1 | -1/+1 |
| | |||||
* | Improving SMT-LIB parser. | Alan Mishchenko | 2016-05-23 | 6 | -27/+38 |
| | |||||
* | Improving SMT-LIB parser. | Alan Mishchenko | 2016-05-21 | 8 | -107/+164 |
| | |||||
* | Improving SMT-LIB parser. | Alan Mishchenko | 2016-05-20 | 6 | -83/+88 |
| | |||||
* | Enabling AIGs without structural hashing (&get -c to import logic network). | Alan Mishchenko | 2016-05-20 | 5 | -26/+36 |
| | |||||
* | Enabling AIGs without structural hashing. | Alan Mishchenko | 2016-05-20 | 2 | -2/+2 |
| | |||||
* | Enabling AIGs without structural hashing. | Alan Mishchenko | 2016-05-20 | 9 | -27/+41 |
| | |||||
* | Switch &miter -y to convert a two-word miter into a dual-output miter. | Alan Mishchenko | 2016-05-20 | 3 | -23/+55 |
| | |||||
* | Enabling AIGs without structural hashing. | Alan Mishchenko | 2016-05-20 | 14 | -42/+60 |
| | |||||
* | Merged in boschmitt/abc (pull request #26) | Alan Mishchenko | 2016-05-19 | 1 | -2/+2 |
|\ | | | | | | | Fix the problem of not identifying divisors when its originating cubes had only 2 literals. | ||||
| * | Merged alanmi/abc into default | Bruno Schmitt | 2016-05-19 | 15 | -61/+962 |
| |\ | |||||
| * | | Fix the problem of not identifying divisors when its originating cubes had ↵ | Bruno Schmitt | 2016-05-19 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | only 2 literals. With this change, 'empty' sub-cubes (sub-cubes with an ID equal to zero) are inserted in the 0th bin of the hash table. | ||||
* | | | Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver. | Alan Mishchenko | 2016-05-19 | 6 | -6/+13 |
| | | | |||||
* | | | Improving SMT-LIB parser. | Alan Mishchenko | 2016-05-19 | 2 | -2/+372 |
| |/ |/| | |||||
* | | New feature for area minimization in standard cell mapping. | Alan Mishchenko | 2016-05-19 | 4 | -1/+392 |
| | | |||||
* | | fix end of line problem that prevents the cmake build system from working | Baruch Sterin | 2016-05-17 | 1 | -1/+1 |
| | | |||||
* | | Bug fix in &demiter. | Alan Mishchenko | 2016-05-16 | 2 | -17/+10 |
| | | |||||
* | | Factoring out library preprocessing code in &nf and putting it elsewhere. | Alan Mishchenko | 2016-05-16 | 5 | -34/+86 |
| | | |||||
* | | Added switch 'read_genlib -n' to anonymize Genlib library. | Alan Mishchenko | 2016-05-16 | 3 | -9/+139 |
| | | |||||
* | | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-15 | 1 | -1/+1 |
| | | |||||
* | | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-15 | 1 | -0/+1 |
| | | |||||
* | | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-15 | 1 | -4/+0 |
| | | |||||
* | | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-15 | 1 | -0/+142 |
| | | |||||
* | | Experiments with generating sat assignments. | Alan Mishchenko | 2016-05-14 | 2 | -0/+196 |
|/ | |||||
* | Adding switch -r to &dch to prevent combo-loops. | Alan Mishchenko | 2016-05-13 | 1 | -3/+7 |
| | |||||
* | New command 'expand' to expand SOPs against the offset. | Alan Mishchenko | 2016-05-12 | 3 | -1/+262 |
| | |||||
* | Adding 'read_pla -d' to read dc-set along with on-set (useful to derive offset). | Alan Mishchenko | 2016-05-12 | 4 | -15/+30 |
| | |||||
* | Cosmetic changes after incorporating new code of 'fxch'. | Alan Mishchenko | 2016-05-11 | 1 | -1/+1 |
| | |||||
* | Cosmetic changes after incorporating new code of 'fxch'. | Alan Mishchenko | 2016-05-11 | 2 | -3/+3 |
| | |||||
* | Cosmetic changes after incorporating new code of 'fxch'. | Alan Mishchenko | 2016-05-11 | 6 | -55/+89 |
| | |||||
* | Add a new module which implements the fast extract with cube hashing (fxch) ↵ | Bruno Schmitt | 2016-05-11 | 10 | -38/+2079 |
| | | | | | | algorithm. Removes old partial implementation of this algorithm from the "pla" module. | ||||
* | Experiments with CEC for arithmetic circuits. | Alan Mishchenko | 2016-05-11 | 11 | -74/+169 |
| | |||||
* | Invalidate packing after mapping is updated. | Alan Mishchenko | 2016-05-09 | 1 | -0/+1 |
| | |||||
* | Experiments with CEC for arithmetic circuits. | Alan Mishchenko | 2016-05-08 | 9 | -136/+447 |
| | |||||
* | Experiments with CEC for arithmetic circuits. | Alan Mishchenko | 2016-05-07 | 1 | -1/+1 |
| | |||||
* | Experiments with CEC for arithmetic circuits. | Alan Mishchenko | 2016-05-07 | 23 | -276/+1405 |
| | |||||
* | Small changes. | Alan Mishchenko | 2016-05-04 | 1 | -2/+2 |
| | |||||
* | Update to &show to show AIGs with XORs and MUXes (derived by &st -m). | Alan Mishchenko | 2016-05-04 | 2 | -1/+2 |
| | |||||
* | Update to &show to show AIGs with XORs and MUXes (derived by &st -m). | Alan Mishchenko | 2016-05-04 | 2 | -4/+30 |
| | |||||
* | Updating GIG parser. | Alan Mishchenko | 2016-05-01 | 3 | -182/+386 |
| | |||||
* | Fanout restriction in &edge. | Alan Mishchenko | 2016-04-30 | 2 | -16/+48 |
| | |||||
* | This code was accidentally deleted from the SAT solver (effectively ↵ | Alan Mishchenko | 2016-04-30 | 1 | -0/+7 |
| | | | | disabling restarts!) | ||||
* | Suggested bug fix in st__strhash(). | Alan Mishchenko | 2016-04-30 | 1 | -7/+6 |
| | |||||
* | Experiments with arithmetic circuits. | Alan Mishchenko | 2016-04-28 | 4 | -4/+301 |
| | |||||
* | Adding option to rehash AIG after mapping. | Alan Mishchenko | 2016-04-27 | 13 | -21/+22 |
| | |||||
* | Extending &satlut to work for 6-LUTs. | Alan Mishchenko | 2016-04-27 | 2 | -9/+17 |
| | |||||
* | Adding missing code to 'dress'. | Alan Mishchenko | 2016-04-27 | 1 | -0/+65 |
| | |||||
* | Using seed assignment of edges in &edge. | Alan Mishchenko | 2016-04-27 | 3 | -2/+17 |
| | |||||
* | Bug fix in bit-blasting of remainder. | Alan Mishchenko | 2016-04-26 | 1 | -1/+1 |
| |