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.
Reset simplify and expression hashmaps when clearing.
If a hashmap got very big, some methods like clear would take a long time (using the hasmap that is linked to on my machine). The clear()
function traverses each of the buckets in the hashmap seeing whether it had children. If the hashmap previously had millions of elements, even if it
now contains just a single element, then there would still be millions of buckets. The clear() function would take much longer than it needed to.
These changes were inspired by testcase15.stp.smt. On my machine, this patch speeds up STP on that benchmark by 20 times.
smccam [Fri, 13 Feb 2009 01:36:20 +0000 (01:36 +0000)]
Fix a couple of memory leaks that existed even if you did
vc_Destroy(): make a constant table used in the bitvector code static,
and delete temporary ASTNode objects in vc_simplify. A simple
createVC, build expression, simplify, destroy loop (test included) now
can run forever without leaking.
trevor_hansen [Tue, 6 Jan 2009 12:38:33 +0000 (12:38 +0000)]
Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM.
Now left shifts by a variable amount. Previously the shift amount needed to a constant.
The smtlib parser reads bitvector constants into strings rather than into ints. This allows formula to
contain constants greater than the size of the machine's integer.
Fixed zero_extend. I didn't add code for it into the SimplifyTermAux function. SBVREM was sometimes failing
because it also wasn't included in the same function. Added it in. Not sure what the function does though..
trevor_hansen [Tue, 6 Jan 2009 02:31:09 +0000 (02:31 +0000)]
Fix compiling of the SMT-LIB Parser, Fix regression test script on bash.
The make files for the smtlib parser referred to to old locations of the SAT solver. The regression tests used
lots to many arguments to ulimit, it didn't run in my bash shell.
katelman [Tue, 30 Dec 2008 06:17:29 +0000 (06:17 +0000)]
Fixed correctness bug in TermToConstTermUsingModel. CounterExampleMap
originally gets a copy of SubstitutionMap by way of SolverMap, and since
SubstitutionMap may not have fully reduced terms, we need to call
TermToConstTermUsingModel on anything read from CounterExampleMap. This was not
done for an array read case.
smccam [Fri, 31 Oct 2008 23:28:04 +0000 (23:28 +0000)]
Add an OPTIMIZE Makefile flag to make it easier to enable optimization
or debugging without otherwise breaking the build. Plus some other
cosmetic changes to Makefile comments.
smccam [Fri, 31 Oct 2008 18:45:04 +0000 (18:45 +0000)]
Remove from SVN files that are automatically generated in the
configure and build processes. Copy the changes to Makefile back to
the original Makefile.in. After this change, you'll need to re-run
"configure".
katelman [Wed, 22 Oct 2008 19:18:17 +0000 (19:18 +0000)]
Round $n$ as I try to incorporate my work from the summer. Major updates
include (a) the newest version of MiniSat, (b) improved CNF conversion, and (c)
various other improvements.
projects / francis / stp.git / log