Baruch Sterin
5ab3f0fa6b
Patch by Larry Doolittle to allow out-of-source builds of ABC.
...
Usage:
Starting from an empty directory:
(1) set AS to point to the location of ABC
(2) reconstruct the directory structure of ABC in the new directory:
mkdir -p `cd $AS && find src -type d`
(3) Build ABC:
make -f $AS/Makefile VPATH=$AS ABCSRC=$AS
2017-10-20 14:41:30 -07:00
Alan Mishchenko
15908929ca
Adding random search in exact synthesis.
2017-10-20 07:49:01 +09:00
Alan Mishchenko
8f690fe862
Integrating old SAT solver into majexact and twoexact.
2017-10-19 13:38:09 +09:00
Alan Mishchenko
298ec14efa
Integrating Glucose into &qbf.
2017-10-17 14:09:41 +09:00
Alan Mishchenko
c1b4b79e99
Integrating Glucose into &qbf.
2017-10-17 13:53:48 +09:00
Alan Mishchenko
1e1d41f3b8
Fix typo on the message reporting max output load.
2017-10-11 18:14:03 +07:00
Alan Mishchenko
222d7c7a92
Fix the build.
2017-10-11 18:12:20 +07:00
Alan Mishchenko
711ea3dfec
Another variation on exact synthesis.
2017-10-11 18:07:35 +07:00
Alan Mishchenko
f97b8d2882
Improvements to SAT based SOP computation.
2017-10-06 17:16:16 +03:00
Alan Mishchenko
02972e53c2
Improvements to truth table manipulation.
2017-10-05 22:39:38 +03:00
Alan Mishchenko
fbdf438d26
Experiments with SAT-based quantification.
2017-10-04 20:02:05 +03:00
Alan Mishchenko
0a3af509bc
Experiments with SAT-based quantification.
2017-10-04 19:10:00 +03:00
Alan Mishchenko
396215532c
Updates and bug fixes.
2017-10-04 12:37:38 +03:00
Alan Mishchenko
343f77a395
Valgrind-ispired fix in CUDD by Kai-hui Chang.
2017-10-03 19:14:27 +03:00
Alan Mishchenko
21aa0ee0e8
Addressing recently reported Bitbucket Issue #72 and #73 .
2017-10-03 16:20:10 +03:00
Alan Mishchenko
d0286dce37
Fixing minimize_assuptions using Glucose.
2017-10-02 21:31:34 +03:00
Alan Mishchenko
05ca7dbf47
Adding printout of slack distribution for mapped networks.
2017-10-02 13:44:48 +03:00
Alan Mishchenko
c272188946
Exact synthesis of majority gates.
2017-10-01 19:49:28 +03:00
Alan Mishchenko
ce8dbc4ac6
Exact synthesis of majority gates.
2017-10-01 18:40:30 +03:00
Alan Mishchenko
d3152aefa7
Exact synthesis of majority gates.
2017-10-01 18:00:09 +03:00
Alan Mishchenko
c696ae95d0
Maintenance and updates.
2017-09-24 23:38:01 -07:00
Alan Mishchenko
287f9efcce
Maintenance and updates.
2017-09-20 19:27:46 -07:00
Alan Mishchenko
1e0bbef1ef
Uncommenting handling of initial values of the flops.
2017-09-19 17:29:03 -07:00
Alan Mishchenko
5585ce8aa6
Enabling Glucose in SAT sweeping: &fraig -g.
2017-09-18 09:37:20 -07:00
Alan Mishchenko
36858c5365
Enabling Glucose in SAT sweeping: &fraig -g.
2017-09-18 09:36:08 -07:00
Alan Mishchenko
12d21480de
Changes to Glucose to enable resetting the solver.
2017-09-18 08:43:55 -07:00
Alan Mishchenko
3a1032c151
Maintenance and updates.
2017-09-18 08:27:05 -07:00
Alan Mishchenko
7e7ba1562e
Compiler warning.
2017-09-16 14:30:02 -07:00
Alan Mishchenko
e7def3d4a2
Enabling variable elim in &bmcs -g.
2017-09-16 14:28:32 -07:00
Alan Mishchenko
b5d42e8bf3
Adding support for Dimacs input to &satoko.
2017-09-16 13:13:30 -07:00
Alan Mishchenko
6d2efdf28f
Improvements in Glucose integration.
2017-09-16 12:48:23 -07:00
Alan Mishchenko
f5cb9d6448
Bug fix in Glucose integration.
2017-09-16 12:37:27 -07:00
Baruch Sterin
adce11979f
bridge relates: (1) fix netlist reader to read the latest version written by ZZ, (2) replace printf() with Abc_Print() in pdr so that it will not interfer with bridge messages
2017-09-15 23:28:57 -07:00
Alan Mishchenko
2da820455e
Undoing updates to &bmcs to help debugging.
2017-09-15 20:54:27 -07:00
Alan Mishchenko
b63e3ee4b4
Experiment with mapping.
2017-09-15 12:40:43 -07:00
Alan Mishchenko
50bed57cae
Changes and fixed suggested by Clifford Wolf.
2017-09-15 10:59:39 -07:00
Alan Mishchenko
4c0b78cf7f
Updates to &bmcs to help debugging.
2017-09-12 11:43:14 -07:00
Alan Mishchenko
efbf5208a2
Adding switch '-c' to 'dsec' to disable internal netlist check.
2017-09-09 08:24:57 -07:00
Alan Mishchenko
f1b7f9062e
Experiments with Glucose.
2017-09-07 23:02:26 -07:00
Alan Mishchenko
03e7b7209e
Experiments with Glucose.
2017-09-07 22:59:59 -07:00
Alan Mishchenko
32312c43f8
Avoid command name collision.
2017-09-07 19:58:34 -07:00
Alan Mishchenko
4cbc97a464
Compiler warnings.
2017-09-07 19:57:29 -07:00
Alan Mishchenko
8a11c911ab
Compiler warnings.
2017-09-07 19:54:12 -07:00
Alan Mishchenko
7ce7e9ec31
Compiler warnings.
2017-09-07 19:45:02 -07:00
Alan Mishchenko
af4c76e21a
Disabling CNF simplification in &bmcs -g.
2017-09-07 19:37:46 -07:00
Alan Mishchenko
ba0d855fd4
Trying to enable CNF simplification in &bmcs -g.
2017-09-07 19:16:13 -07:00
Alan Mishchenko
68b59b8a1e
Bug fix: forgot to init the runtime limit in Glucose.
2017-09-06 20:55:16 -07:00
Alan Mishchenko
3ffb098d64
Adding global conflict counter to Satoko (to make it apple-to-apple with other solvers).
2017-09-06 20:33:53 -07:00
Alan Mishchenko
97dd6019bf
Integrating Glucose into bmc3 -g.
2017-09-06 19:56:53 -07:00
Alan Mishchenko
b1bf802fda
More renaming.
2017-09-06 18:46:12 -07:00