]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
projects / francis / stp.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b311fc8) | patch
Speedups.
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 26 Jun 2010 08:44:09 +0000 (08:44 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Sat, 26 Jun 2010 08:44:09 +0000 (08:44 +0000)
commit7e379dccc8cee7dbb7d0829448a984d6d350a9f1
tree5381f003f6ca754ccd2992d55ad0133626899989tree | snapshot
parentb311fc813f32f0ea4cbfd62a6fdedc27f1675b62commit | diff
Speedups.

* The substitution map now substitutes for (IFF SYMBOL SYMBOL)
* sim.smt2 is the test case to check the above substitution is working.
* The ArrayTransformer creates fewer new nodes.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@889 e59a4935-1847-0410-ae03-e826735625c1
src/AST/ArrayTransformer.cpp diff | blob | history
src/simplifier/SubstitutionMap.cpp diff | blob | history
src/simplifier/SubstitutionMap.h diff | blob | history
unit_test/output_0.cnf [deleted file] blob | history
unit_test/sim.smt2 [new file with mode: 0644] blob
unit_test/unit_test.sh diff | blob | history
STP Constraint Solver.