summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abc.c
Commit message (Expand)AuthorAgeFilesLines
* Variable timeframe abstraction.Alan Mishchenko2012-01-271-2/+14
* Variable timeframe abstraction.Alan Mishchenko2012-01-271-1/+1
* Variable timeframe abstraction.Alan Mishchenko2012-01-241-2/+2
* Variable timeframe abstraction.Alan Mishchenko2012-01-231-1/+1
* Major restructuring of the code.Alan Mishchenko2012-01-211-3226/+42
* Preserving CI/CO varible names when moving between the main space and &-space.Alan Mishchenko2012-01-201-8/+25
* Variable timeframe abstraction.Alan Mishchenko2012-01-201-2/+59
* New hierarchy manager.Alan Mishchenko2012-01-191-5/+16
* Replaced 'bmc' by 'bmc2' in 'dprove'. Added switches to 'dprove' to control B...Alan Mishchenko2012-01-191-4/+30
* New hierarchy manager.Alan Mishchenko2012-01-171-1/+72
* Variable timeframe abstraction.Alan Mishchenko2012-01-161-2/+120
* Variable timeframe abstraction.Alan Mishchenko2012-01-151-6/+4
* Changes to the lazy man's synthesis code.Alan Mishchenko2012-01-141-3/+6
* New hierarchy manager.Alan Mishchenko2012-01-141-2/+8
* New hierarchy manager.Alan Mishchenko2012-01-131-0/+2
* Changes to the lazy man's synthesis code.Alan Mishchenko2012-01-111-1/+47
* Gate level abstraction.Alan Mishchenko2012-01-081-3/+6
* Bug fix: changing output number to 0 in the CEX after ORing POs.Alan Mishchenko2012-01-071-0/+3
* Backward reachability using circuit cofactoring.Alan Mishchenko2012-01-011-3/+106
* Delay optimization using precomputed library.Alan Mishchenko2011-12-291-30/+100
* New variable-time frame abstraction.Alan Mishchenko2011-12-291-8/+6
* Added switch -n to 'miter' to ignore PI/PO names.Alan Mishchenko2011-12-221-3/+15
* Computing interpolants as truth tables.Alan Mishchenko2011-12-221-1/+2
* Adding switch '-W' to fx to control the quality of extracted divisors.Alan Mishchenko2011-12-151-4/+16
* Started SAT-based reparameterization.Alan Mishchenko2011-12-131-2/+3
* Added command &read_blif to read hierarchical BLIF directly into the &-space.Alan Mishchenko2011-12-121-0/+71
* Integrated new proof-logging into proof-based gate-level abstraction.Alan Mishchenko2011-12-081-3/+8
* Added recording of AIG subgraphs.Alan Mishchenko2011-12-061-13/+12
* Started experiments with a new solver.Alan Mishchenko2011-11-251-6/+12
* Making GLA PBA and GLA CBA communicate information.Alan Mishchenko2011-11-221-7/+6
* Enabled skipping random decisions in PBA, which are performed by default.Alan Mishchenko2011-11-121-2/+7
* Do not allow interpolation with constraints.Alan Mishchenko2011-11-121-0/+5
* Dump inductive invariant or last interpolant after interpolation.Alan Mishchenko2011-11-121-2/+6
* Enabled counter-example minimization in 'write_counter'.Alan Mishchenko2011-11-111-1/+1
* Changing defaults in gate-level abstraction.Alan Mishchenko2011-11-061-5/+6
* Changes to read multi-output testcases described using AIGER 1.9.Alan Mishchenko2011-11-061-10/+21
* C++ portability changes.Alan Mishchenko2011-10-271-1/+1
* Improvements to the new abstraction code.Alan Mishchenko2011-10-271-10/+21
* New proof-based abstraction code.Alan Mishchenko2011-10-251-5/+128
* Improvements to the QBF solver.Alan Mishchenko2011-10-251-5/+19
* Improvements to the QBF solver.Alan Mishchenko2011-10-241-6/+32
* New abstraction code.Alan Mishchenko2011-10-191-0/+5
* New abstraction code.Alan Mishchenko2011-10-191-4/+4
* New abstraction code.Alan Mishchenko2011-10-191-4/+8
* New abstraction code.Alan Mishchenko2011-10-151-11/+12
* Changes to the matching procedure.Alan Mishchenko2011-10-061-2/+2
* Changes to the matching procedure.Alan Mishchenko2011-10-011-5/+15
* Changes to the matching procedure and new abstraction code.Alan Mishchenko2011-09-271-4/+17
* Changes to Boolean matching.Alan Mishchenko2011-09-241-2/+48
* Added new feature to bmc3.Alan Mishchenko2011-09-231-3/+27
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-27 16:06:46 +0000