]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 22d1f43) | patch
First step of integrating Bitblasting to AIGs.
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 1 Mar 2010 15:03:22 +0000 (15:03 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 1 Mar 2010 15:03:22 +0000 (15:03 +0000)
commit449137798aa0ca44014f4f2fa51fe7fb32042a86
treed859c7e3fb69458b57bdbc35daf9ff049e1107aetree | snapshot
parent22d1f43d663718d48483e40d5b52a05960f49f09commit | diff
First step of integrating Bitblasting to AIGs.
* The Bitblaster now produces BBNodes, not ASTNodes. Currently BBNodes are typedefed to ASTNodes.
* Improvements were made to the trunk's Bitblaster while I was working on this. I'll merge them in next.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@622 e59a4935-1847-0410-ae03-e826735625c1
src/to-sat/BBNode.h [new file with mode: 0644] blob
src/to-sat/BBNodeManager.h [new file with mode: 0644] blob
src/to-sat/BitBlastNew.cpp [new file with mode: 0644] blob
src/to-sat/BitBlastNew.h [new file with mode: 0644] blob
src/to-sat/CallSAT.cpp diff | blob | history
src/to-sat/ToSAT.h diff | blob | history
src/to-sat/old/BitBlast.cpp [moved from src/to-sat/BitBlast.cpp with 100% similarity] blob | history
src/to-sat/old/BitBlast.h [moved from src/to-sat/BitBlast.h with 100% similarity] blob | history
STP Constraint Solver.