]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times.
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 18 Apr 2009 15:23:04 +0000 (15:23 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 18 Apr 2009 15:23:04 +0000 (15:23 +0000)
commit439c511e86728f4f12cb8434617b758d47ffd910
tree11bb2457c8ea663ffd4339bc15041f806b27e96b
parent5c05c30f0cd66304d1102393f9b71d462ae47c09
Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times.

* Some SMT-LIB format outputting of expression.
* Parsing arbitary length bitvector input strings via the C-interface.
* No more memory leaks from the _letid_expr_map & co.
* const& to reduce copy constructor usage in BVTypeCheck.
* Checks for equality on some fixed bits. e.g. (= bv0[16] (concat bv1[15] x)) == false.
* Reduces multiplications with leading 1's to a minus. e.g. 255*x == -1*x.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@68 e59a4935-1847-0410-ae03-e826735625c1
AST/AST.cpp
AST/AST.h
c_interface/c_interface.cpp
c_interface/c_interface.h
simplifier/simplifier.cpp