Alan Mishchenko
|
f75e55bb4b
|
Fixed &reachy to perform reparametrization in case reachability is disabled.
|
2011-11-03 19:32:20 -05:00 |
Alan Mishchenko
|
5b75410a5e
|
Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.
|
2011-10-31 15:04:47 -05:00 |
Alan Mishchenko
|
868a1b9aeb
|
Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.
|
2011-10-31 14:59:47 -05:00 |
Alan Mishchenko
|
f08be2742e
|
C++ portability changes.
|
2011-10-27 23:34:11 -07:00 |
Alan Mishchenko
|
24d27e5524
|
Improvements to the new abstraction code.
|
2011-10-27 22:27:00 -07:00 |
Alan Mishchenko
|
ef288ed5d0
|
Removed some recently added file, which broke compilation.
|
2011-10-27 14:28:41 -07:00 |
Alan Mishchenko
|
0ff0a552a5
|
Improvements to the new abstraction code.
|
2011-10-27 14:23:43 -07:00 |
Alan Mishchenko
|
bc81cf2dae
|
Improvements to the new abstraction code.
|
2011-10-27 14:20:47 -07:00 |
Alan Mishchenko
|
1dcdba1bee
|
New proof-based abstraction code (bug fix).
|
2011-10-27 10:10:10 -07:00 |
Alan Mishchenko
|
0736f39609
|
New truth table permutation procedure.
|
2011-10-26 23:15:42 +08:00 |
Alan Mishchenko
|
0f77840520
|
New proof-based abstraction code.
|
2011-10-25 18:32:06 +08:00 |
Alan Mishchenko
|
f7fd329787
|
Improvements to the QBF solver.
|
2011-10-25 17:22:33 +08:00 |
Alan Mishchenko
|
a8e1ba40b9
|
The result of merging with recent PyABC changes.
|
2011-10-25 14:05:50 +08:00 |
Baruch Sterin
|
b51ab36922
|
pyabc: minor changes for compeition
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
a6d6a40ff3
|
pyabc: add additional scripts for HWMCC11 competition
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
89ac9abe75
|
pyabc: updated Bob's scripts
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
15d0d84bb4
|
pyabc: rearrange files and locations
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
521ec0fcf9
|
pyabc: fix command line parser in reachx_cmx.py and abcpy_test.py
|
2011-10-24 15:21:08 -07:00 |
Alan Mishchenko
|
f96f3fa583
|
Improvements to the QBF solver.
|
2011-10-24 18:05:45 +08:00 |
Alan Mishchenko
|
88c36d9d65
|
New abstraction code (bug fix).
|
2011-10-23 13:20:24 +07:00 |
Alan Mishchenko
|
9ec9d9f315
|
New abstraction code.
|
2011-10-19 23:45:11 +07:00 |
Alan Mishchenko
|
19ce8396f0
|
New abstraction code.
|
2011-10-19 16:03:15 +07:00 |
Alan Mishchenko
|
397bebf8a5
|
New abstraction code.
|
2011-10-19 15:42:55 +07:00 |
Alan Mishchenko
|
efd310af3e
|
Skip NULL entry when freeing vector of vectors.
|
2011-10-19 14:22:33 +07:00 |
Alan Mishchenko
|
5dbfc74807
|
Changes to CNF generation code.
|
2011-10-19 14:21:41 +07:00 |
Alan Mishchenko
|
1d0b827603
|
Changes to CNF generation code.
|
2011-10-19 11:49:54 +07:00 |
Alan Mishchenko
|
12b70d4946
|
Changes to CNF generation code.
|
2011-10-17 10:39:05 +03:00 |
Alan Mishchenko
|
6f0b87dd5c
|
New abstraction code.
|
2011-10-15 22:04:05 +03:00 |
Alan Mishchenko
|
e4bd4d5440
|
New abstraction code.
|
2011-10-14 16:49:43 +03:00 |
Alan Mishchenko
|
c6982485e4
|
New abstraction code.
|
2011-10-14 16:48:45 +03:00 |
Alan Mishchenko
|
ad5ee9ff46
|
Changes to the matching procedure.
|
2011-10-12 15:04:41 +03:00 |
Alan Mishchenko
|
191de3e885
|
Changes to the matching procedure.
|
2011-10-10 22:19:34 +03:00 |
Alan Mishchenko
|
657f2acd71
|
Changes to the matching procedure.
|
2011-10-10 21:55:32 +03:00 |
Alan Mishchenko
|
9daabedff5
|
Fixing built-in resource limit when converting truth-tables to AIGs.
|
2011-10-08 23:18:44 +07:00 |
Alan Mishchenko
|
924ec940fe
|
Changes to the matching procedure.
|
2011-10-06 15:48:27 +07:00 |
Alan Mishchenko
|
d66b586330
|
Modified write_blif to output LUT structures.
|
2011-10-04 18:43:23 +07:00 |
Alan Mishchenko
|
8c302870f4
|
Changes to the matching procedure.
|
2011-10-03 13:34:17 +07:00 |
Alan Mishchenko
|
0f9dacb7be
|
Changes to the matching procedure.
|
2011-10-02 16:39:51 +07:00 |
Alan Mishchenko
|
e6e6a3cf9e
|
Changes to the matching procedure.
|
2011-10-01 17:00:59 +07:00 |
Alan Mishchenko
|
ff4c674dd7
|
Updated miter status check to detect the case when a PO is equal to a true PI.
|
2011-10-01 10:51:33 +07:00 |
Alan Mishchenko
|
7884dd01bc
|
Fixed a corner case bug in dprove when a trivial CEX is not produced.
|
2011-10-01 10:50:50 +07:00 |
Alan Mishchenko
|
dbe2b466d7
|
Added handling of exceeding conflict limit in PushClasses.
|
2011-10-01 08:00:04 +07:00 |
Baruch Sterin
|
16e12f1852
|
pyabc: fix callbacks into python to work correctly by moving to PyGILEState_Ensure/Release APIs
|
2011-09-29 17:34:05 -07:00 |
Baruch Sterin
|
ef0fbf0372
|
completely silence the "source" command when the -s option is given
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
9d652062b7
|
pyabc: fix indentation in pyabc.i
|
2011-10-24 15:21:08 -07:00 |
Baruch Sterin
|
e9ef8e97bf
|
Makefile: current LIBS line has a lot of unnecessary and problematic stuff. Replace it with just "-lreadline"
|
2011-10-24 15:21:08 -07:00 |
Alan Mishchenko
|
519b03e8e8
|
Changes to the matching procedure and new abstraction code.
|
2011-09-27 15:10:53 +07:00 |
Alan Mishchenko
|
976f5f5a12
|
Changes to Boolean matching.
|
2011-09-24 20:15:54 -07:00 |
Alan Mishchenko
|
d080336bb5
|
Added new feature to bmc3.
|
2011-09-23 22:35:03 -07:00 |
Alan Mishchenko
|
8f74276edb
|
Initial changes to enable gate-level abstraction.
|
2011-09-22 09:37:44 -07:00 |