summaryrefslogtreecommitdiffstats
path: root/src/base
Commit message (Expand)AuthorAgeFilesLines
* Trying to make sorting of nodes platform-indendent.Alan Mishchenko2011-12-153-0/+15
* Trying to make sorting of nodes platform-indendent.Alan Mishchenko2011-12-151-0/+5
* Started SAT-based reparameterization.Alan Mishchenko2011-12-131-2/+3
* g++ portability changes.Alan Mishchenko2011-12-131-1/+1
* Added command &read_blif to read hierarchical BLIF directly into the &-space.Alan Mishchenko2011-12-121-0/+47
* Added command &read_blif to read hierarchical BLIF directly into the &-space.Alan Mishchenko2011-12-126-2/+442
* Added the hierarchy printout.Alan Mishchenko2011-12-111-0/+100
* Added support for generating a library of real-life truth-tables.Alan Mishchenko2011-12-091-6/+6
* Added support for generating a library of real-life truth-tables.Alan Mishchenko2011-12-091-2/+0
* Added support for generating a library of real-life truth-tables.Alan Mishchenko2011-12-093-6/+50
* Integrated new proof-logging into proof-based gate-level abstraction.Alan Mishchenko2011-12-081-3/+8
* g++ portability changes.Alan Mishchenko2011-12-061-18/+18
* Added recording of AIG subgraphs.Alan Mishchenko2011-12-061-9/+9
* Added recording of AIG subgraphs.Alan Mishchenko2011-12-061-0/+1
* Performance bug fix in SOP balancing.Alan Mishchenko2011-12-061-1/+1
* Added recording of AIG subgraphs.Alan Mishchenko2011-12-063-22/+22
* Started experiments with a new solver.Alan Mishchenko2011-11-254-14/+20
* Making GLA PBA and GLA CBA communicate information.Alan Mishchenko2011-11-221-7/+6
* Temporary debugging change.Alan Mishchenko2011-11-121-1/+1
* 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-112-6/+32
* Preventing scripts from aborting if reading has failed.Alan Mishchenko2011-11-081-1/+1
* Corner case bug in deriving truth table from SOP.Alan Mishchenko2011-11-081-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-065-37/+167
* Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.Alan Mishchenko2011-10-311-5/+5
* C++ portability changes.Alan Mishchenko2011-10-273-6/+3
* 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-253-9/+38
* The result of merging with recent PyABC changes.Alan Mishchenko2011-10-251-1/+1
|\
| * completely silence the "source" command when the -s option is givenBaruch Sterin2011-10-241-1/+1
* | Improvements to the QBF solver.Alan Mishchenko2011-10-243-10/+59
|/
* 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
* Changes to CNF generation code.Alan Mishchenko2011-10-172-11/+44
* New abstraction code.Alan Mishchenko2011-10-151-11/+12
* Changes to the matching procedure.Alan Mishchenko2011-10-121-36/+58
* Changes to the matching procedure.Alan Mishchenko2011-10-061-2/+2
* Modified write_blif to output LUT structures.Alan Mishchenko2011-10-045-13/+230
* 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-242-3/+49
* Added new feature to bmc3.Alan Mishchenko2011-09-231-3/+27
* Initial changes to enable gate-level abstraction.Alan Mishchenko2011-09-221-14/+205
* 64-bit portability changes.Alan Mishchenko2011-09-173-10/+10
* Added limit on the number of flops to add in one iteration of &abs_refine.Alan Mishchenko2011-09-121-11/+24