]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 51a5690) | patch
Add the parts of the ABC system for sequential synthesis and verification that handle...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 6 Mar 2010 13:48:41 +0000 (13:48 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 6 Mar 2010 13:48:41 +0000 (13:48 +0000)
commitbd51563c75f57d55b870c35081bef01e5a415263
tree18938ba62e5a9d3158b4ead3b0d2f21ae9da3d9btree | snapshot
parent51a56904815209ca6fdb2a1b9dc697cbf61bc2e1commit | diff
Add the parts of the ABC system for sequential synthesis and verification that handles AIG (and-inverter graphs). This is just code related to managing AIGS and outputting them to CNF. This is version 070930 with only a syntactic change to remove a Valgrind warning.

NB: This is just the library. I haven't checked in the changes to STP to use the library.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@625 e59a4935-1847-0410-ae03-e826735625c1
72 files changed:
LICENSE_COMPONENTS [new file with mode: 0644] blob
Makefile diff | blob | history
scripts/Makefile.in diff | blob | history
src/extlib-abc/Makefile [new file with mode: 0644] blob
src/extlib-abc/aig.h [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigCheck.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigDfs.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigFanout.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigMan.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigMem.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigMffc.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigObj.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigOper.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigOrder.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigPart.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigRepr.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigRet.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigScl.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigSeq.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigShow.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigTable.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigTime.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigTiming.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigTruth.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigTsim.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigUtil.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aigWin.c [new file with mode: 0644] blob
src/extlib-abc/aig/aig/aig_.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/Makefile [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfCore.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfCut.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfData.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfMan.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfMap.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfPost.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfUtil.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnfWrite.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/cnf_.c [new file with mode: 0644] blob
src/extlib-abc/aig/cnf/module.make [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darBalance.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darCore.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darCut.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darData.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darLib.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darMan.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darPrec.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darRefact.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darResub.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/darScript.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/dar_.c [new file with mode: 0644] blob
src/extlib-abc/aig/dar/module.make [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kitAig.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kitGraph.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kitIsop.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kitSop.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kitTruth.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/kit_.c [new file with mode: 0644] blob
src/extlib-abc/aig/kit/module.make [new file with mode: 0644] blob
src/extlib-abc/cnf.h [new file with mode: 0644] blob
src/extlib-abc/cnf_short.h [new file with mode: 0644] blob
src/extlib-abc/copyright.txt [new file with mode: 0644] blob
src/extlib-abc/dar.h [new file with mode: 0644] blob
src/extlib-abc/darInt.h [new file with mode: 0644] blob
src/extlib-abc/kit.h [new file with mode: 0644] blob
src/extlib-abc/leaks.h [new file with mode: 0644] blob
src/extlib-abc/vec.h [new file with mode: 0644] blob
src/extlib-abc/vecAtt.h [new file with mode: 0644] blob
src/extlib-abc/vecFlt.h [new file with mode: 0644] blob
src/extlib-abc/vecInt.h [new file with mode: 0644] blob
src/extlib-abc/vecPtr.h [new file with mode: 0644] blob
src/extlib-abc/vecStr.h [new file with mode: 0644] blob
src/extlib-abc/vecVec.h [new file with mode: 0644] blob
STP Constraint Solver.