Alan Mishchenko
8bfe8d5210
Adding a debug way to print cuts used in the CNF-generator.
2016-07-13 10:35:02 -07:00
Alan Mishchenko
42ae280089
Removing verbose output in &cec and &syn4.
2016-07-13 09:00:39 -07:00
Alan Mishchenko
3b76bc2792
Bug-fix in SMT-LIB parser (incorrect handling of arithmetic right-shift).
2016-07-12 13:34:06 -07:00
Alan Mishchenko
4ffc14fd56
Small change to make &if not abort the scripts.
2016-07-04 23:54:07 -07:00
Alan Mishchenko
3ad4be259e
Bit-blasting Booth multipliers.
2016-07-04 20:41:50 -07:00
Alan Mishchenko
f3ecc3ffaa
Experiments with edge-based mapping (bug fix).
2016-07-02 12:14:18 -07:00
Alan Mishchenko
84a277b491
Bug fix in blasting shifters with large bit-width.
2016-06-29 15:37:37 -07:00
Alan Mishchenko
d02f9dd4df
Bug fix in blasting shifters with large bit-width.
2016-06-29 15:36:31 -07:00
Alan Mishchenko
7dcba3e27b
Experiments with edge-based mapping.
2016-06-29 15:29:24 -07:00
Alan Mishchenko
688f0269db
Bug fix in blasting shifters with large bit-width.
2016-06-28 09:53:09 -07:00
Alan Mishchenko
a309569390
New multi-output PLA reader and preprocessor (read_plamo) (updated dist-1 merge).
2016-06-17 22:30:54 -07:00
Alan Mishchenko
720d025234
Complier fix.
2016-06-17 21:54:50 -07:00
Alan Mishchenko
22406e7101
Merged in boschmitt/abc (pull request #28 )
...
Handling D1C and SCC in FXCH
2016-06-17 21:53:04 -07:00
Alan Mishchenko
c912875261
New command 'phase_map'.
2016-06-17 20:21:39 -07:00
Alan Mishchenko
92a448e6ab
Experiments with edge-based mapping.
2016-06-17 19:57:30 -07:00
Bruno Schmitt
85428a60cc
Enables FXCH to handle Distance-1 cubes (D1C) and Single Cube Containment (SCC) as by product of extraction.
...
D1C: Whenever they appear a constant divisor (x! + x) will be created and handle as any other divisor.
SCC: Will be taken care of as soon as they appear.
2016-06-17 17:24:58 -03:00
Alan Mishchenko
3c3a770a17
New multi-output PLA reader and preprocessor (read_plamo) (added dist-1 merge).
2016-06-16 21:09:39 -07:00
Alan Mishchenko
e06c04a3ef
Change to BENCH reader to read DFF with four inputs.
2016-06-16 16:48:45 -07:00
Alan Mishchenko
0923d543ad
Adding a switch 'retime -o' to use old flop naming conventions.
2016-06-16 16:13:13 -07:00
Alan Mishchenko
ada21a655f
New multi-output PLA reader and preprocessor (read_plamo).
2016-06-16 15:22:03 -07:00
Alan Mishchenko
e1b51d1863
Experiments with edge-based mapping.
2016-06-15 18:47:10 -07:00
Alan Mishchenko
db43d6fbd8
Adding switch -P <num> to command 'cover'.
2016-06-14 20:43:50 -07:00
Alan Mishchenko
0a1b6f8fcc
Detecting properties of internal nodes.
2016-06-14 15:37:59 -07:00
Alan Mishchenko
a18da5c878
Detecting properties of internal nodes.
2016-06-12 19:07:46 -07:00
Alan Mishchenko
699dd39035
Support bit-blasting of shifts with more than 32 bits (fix).
2016-06-08 22:25:12 -05:00
Alan Mishchenko
cad3d8d419
Support bit-blasting of shifts with more than 32 bits.
2016-06-07 15:20:38 -07:00
Alan Mishchenko
820a48b2cb
Changes to Wlc to accommodate signed signals in SMT-LIB.
2016-06-07 15:05:21 -07:00
Alan Mishchenko
4efbd7b3ca
Detecting properties of internal nodes.
2016-06-07 14:32:38 -07:00
Alan Mishchenko
998aeff15e
Improvement to CNF encoding of cardinality constraints proposed by Mathias Soaken.
2016-06-07 00:22:32 -07:00
Alan Mishchenko
31b2e8bebd
Switch 'fx -x' to use only canonical divisors in 'fx'.
2016-06-06 19:31:56 -07:00
Alan Mishchenko
00242f2fb2
New profiling features for word-level optimizations.
2016-06-04 17:31:15 -07:00
Alan Mishchenko
93c785e802
Small changes for today's experiments.
2016-06-03 13:22:24 -07:00
Alan Mishchenko
e33d6e8d9d
Small changes to compile on Windows.
2016-06-03 10:12:00 -07:00
Bruno Schmitt
fe6a647f37
Merged alanmi/abc into default
2016-06-02 20:30:04 -03:00
Bruno Schmitt
b6ab087952
Removing the memory saving mode, it is no longer necessary.
2016-06-02 17:26:12 -03:00
Bruno Schmitt
4937fb09ed
Minimizing memory usage. The implementation was using twice as much memory as necessary.
2016-06-02 17:23:35 -03:00
Alan Mishchenko
e1b32ee756
Silencing several messages.
2016-06-01 11:57:29 -07:00
Alan Mishchenko
1d26d58a17
Adding switch 'pdr -o' to control using property output in induction.
2016-05-25 13:47:38 -07:00
Alan Mishchenko
58c81ec097
Improving SMT-LIB parser.
2016-05-23 11:15:37 -07:00
Alan Mishchenko
c688d1b158
Improving SMT-LIB parser.
2016-05-23 10:42:53 -07:00
Alan Mishchenko
0f29f0aec9
Improving SMT-LIB parser.
2016-05-21 20:08:05 -07:00
Alan Mishchenko
34c5ac88d4
Improving SMT-LIB parser.
2016-05-20 20:38:43 -07:00
Alan Mishchenko
7b570b6241
Enabling AIGs without structural hashing (&get -c to import logic network).
2016-05-20 18:01:01 -07:00
Alan Mishchenko
ce126db5f5
Enabling AIGs without structural hashing.
2016-05-20 16:37:58 -07:00
Alan Mishchenko
3b62ee4575
Enabling AIGs without structural hashing.
2016-05-20 16:23:48 -07:00
Alan Mishchenko
27c44fd644
Switch &miter -y to convert a two-word miter into a dual-output miter.
2016-05-20 14:03:07 -07:00
Alan Mishchenko
555ed0b158
Enabling AIGs without structural hashing.
2016-05-20 13:50:19 -07:00
Alan Mishchenko
c6a290ee97
Merged in boschmitt/abc (pull request #26 )
...
Fix the problem of not identifying divisors when its originating cubes had only 2 literals.
2016-05-19 23:34:20 -07:00
Alan Mishchenko
2ded89cca5
Added switch 'bmc3 -r' to disable periodic restarts in the SAT solver.
2016-05-19 22:33:40 -07:00
Alan Mishchenko
2d0a8fb4cb
Improving SMT-LIB parser.
2016-05-19 22:07:52 -07:00