Alan Mishchenko
|
da525b2a23
|
Debugging a proof error.
|
2012-07-13 16:25:07 -07:00 |
Alan Mishchenko
|
b7b60ebdcb
|
Fixing a mismatch in regular/shadow page memory appending procedure.
|
2012-07-13 16:10:20 -07:00 |
Alan Mishchenko
|
be95437d1a
|
Debugging a proof error.
|
2012-07-13 15:44:45 -07:00 |
Alan Mishchenko
|
f54bf25d70
|
Debugging a proof error.
|
2012-07-13 15:12:21 -07:00 |
Alan Mishchenko
|
d3ad7fbaf3
|
Several small changes and fixes.
|
2012-07-13 15:02:46 -07:00 |
Alan Mishchenko
|
86a0ae0bca
|
Removed useless file.
|
2012-07-12 19:07:24 -07:00 |
Alan Mishchenko
|
743ab55fad
|
Upgraded &equiv3 to periodically restart simulation from the init state.
|
2012-07-12 18:56:26 -07:00 |
Alan Mishchenko
|
97d2c9a264
|
Added procedure for checking satisfied clauses.
|
2012-07-12 18:55:24 -07:00 |
Alan Mishchenko
|
17305bd563
|
Fixing temporary linker problem.
|
2012-07-12 18:54:44 -07:00 |
Alan Mishchenko
|
83f1f27307
|
Silencing warnings.
|
2012-07-11 15:53:59 -07:00 |
Alan Mishchenko
|
719396a2ff
|
Silencing warnings.
|
2012-07-11 15:52:33 -07:00 |
Alan Mishchenko
|
da02d5aa9d
|
Handling the trivial case when PO is driven by a constant.
|
2012-07-11 15:45:55 -07:00 |
Alan Mishchenko
|
2427563269
|
Changes to clause mapping.
|
2012-07-11 15:33:31 -07:00 |
Alan Mishchenko
|
05c8b78531
|
Changes to clause mapping.
|
2012-07-11 14:05:07 -07:00 |
Alan Mishchenko
|
b9ee5d8564
|
Improvements in the proof-logging SAT solver.
|
2012-07-11 12:45:46 -07:00 |
Alan Mishchenko
|
5f3ba152e5
|
Fixed several problems when CEX is detected by &vta/&gla.
|
2012-07-11 09:31:00 -07:00 |
Alan Mishchenko
|
8dc61f1f20
|
Enabling refinement in &gla_refine even if CEX is invalid.
|
2012-07-11 09:05:20 -07:00 |
Alan Mishchenko
|
63dab64574
|
Replacing printf() by Abc_Print().
|
2012-07-10 18:04:08 -07:00 |
Alan Mishchenko
|
448eec77b7
|
Improving print-outs of &vta and &gla.
|
2012-07-10 13:56:39 -07:00 |
Alan Mishchenko
|
db6e7f97c1
|
Improving print-outs of &vta and &gla.
|
2012-07-10 12:47:47 -07:00 |
Alan Mishchenko
|
1d441b6489
|
Performance bug fix in the SAT solver (clearing variable activity after rollback).
|
2012-07-10 01:26:23 -07:00 |
Alan Mishchenko
|
997e4c77ac
|
Performance bug fix in the SAT solver (clearing variable activity after rollback).
|
2012-07-09 23:15:12 -07:00 |
Alan Mishchenko
|
6ba6c3279a
|
Performance bug fix in the SAT solver (clearing variable activity after rollback).
|
2012-07-09 23:09:59 -07:00 |
Alan Mishchenko
|
908d5e696c
|
Replacing Mb/Gb to be MB/GB.
|
2012-07-09 22:57:03 -07:00 |
Alan Mishchenko
|
d46c49088d
|
Bug fix in the recent changes to the SAT solver.
|
2012-07-09 22:44:38 -07:00 |
Alan Mishchenko
|
b2f1d21d37
|
Removing print-out message.
|
2012-07-09 22:29:24 -07:00 |
Alan Mishchenko
|
a92c41f767
|
Removing print-out message in bridge mode.
|
2012-07-09 22:16:52 -07:00 |
Alan Mishchenko
|
291f1ee054
|
Performance bug fix in &gla.
|
2012-07-09 22:16:23 -07:00 |
Alan Mishchenko
|
637736827a
|
Adding several command-line arguments to 'dsat'.
|
2012-07-09 19:24:39 -07:00 |
Alan Mishchenko
|
22dc498374
|
Updated Python code to reflect change in include files.
|
2012-07-09 17:04:10 -07:00 |
Alan Mishchenko
|
c265d2449a
|
Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).
|
2012-07-09 15:57:18 -07:00 |
Alan Mishchenko
|
685faae8e2
|
Added command &gla_purify.
|
2012-07-08 17:56:49 -07:00 |
Alan Mishchenko
|
21b847a8db
|
Updating truth table computation for GIA to work for internal nodes as well.
|
2012-07-08 14:04:52 -07:00 |
Alan Mishchenko
|
ff0ec52d4d
|
Updating memory print-out of &vta and &gla.
|
2012-07-08 14:01:28 -07:00 |
Alan Mishchenko
|
d533f18219
|
Adding printout to report command line executed in batch mode.
|
2012-07-08 13:23:29 -07:00 |
Alan Mishchenko
|
6c3363f777
|
Adding restart to rarity simulation in sim3 and &sim3.
|
2012-07-08 13:23:05 -07:00 |
Alan Mishchenko
|
e80bd69ed6
|
Adding flushing stdout after printing verbose stats.
|
2012-07-07 20:41:16 -07:00 |
Alan Mishchenko
|
fc574a7c61
|
Adding simple program for executing several instances of ABC in parallel.
|
2012-07-07 20:37:16 -07:00 |
Alan Mishchenko
|
1c33107cbb
|
Updating project settings to have simpler include paths.
|
2012-07-07 20:14:12 -07:00 |
Alan Mishchenko
|
b0ef0aaf00
|
Fixing time primtouts throughout the code.
|
2012-07-07 18:43:04 -07:00 |
Alan Mishchenko
|
ea98a2497e
|
Fixing time primtouts throughout the code.
|
2012-07-07 18:41:02 -07:00 |
Alan Mishchenko
|
4760983a46
|
Fixing time primtouts throughout the code.
|
2012-07-07 18:15:08 -07:00 |
Alan Mishchenko
|
3aab724573
|
Fixing time primtouts throughout the code.
|
2012-07-07 17:46:54 -07:00 |
Alan Mishchenko
|
16d96fcf53
|
Changing the default value of &vta -t to reduce proof memory usage.
|
2012-07-07 14:43:14 -07:00 |
Alan Mishchenko
|
504cdad865
|
Fixing time primtouts in &vta and &gla.
|
2012-07-07 14:40:02 -07:00 |
Alan Mishchenko
|
44f04004fd
|
Adding memory report to print-outs produced by &vta and &gla.
|
2012-07-07 14:33:54 -07:00 |
Alan Mishchenko
|
e22f5d1246
|
Bug fix in &gla_refine.
|
2012-07-07 13:21:54 -07:00 |
Alan Mishchenko
|
5fb7c676c2
|
Procedure to compute truth tables for POs of GIA.
|
2012-07-07 13:13:32 -07:00 |
Alan Mishchenko
|
bea33c0584
|
Diabling compact AIGER writing by default.
|
2012-07-07 12:23:03 -07:00 |
Alan Mishchenko
|
d82142cbe5
|
Fixed &gla to work in the bridge mode.
|
2012-07-07 11:16:42 -07:00 |