]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Sun, 2 Jan 2011 03:57:50 +0000 (03:57 +0000)]
Cleanup / Speedup. Unnecessary work was done when building the counter example.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1047
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 2 Jan 2011 02:29:15 +0000 (02:29 +0000)]
Bugfix. I didn't realise that the Flatten function didn't flatten BVOR/BVANDs. When I replaced the function, it did. Flattening these took a long time. This patch: (1) performs the flatten upfront, (2) allows BVOR/BVAND >2 arity.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1046
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 2 Jan 2011 01:49:16 +0000 (01:49 +0000)]
Refactor. This shouldn't change anything
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1045
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 1 Jan 2011 04:15:27 +0000 (04:15 +0000)]
Speedup. The old Flatten was too slow. On an instance of binary AND nodes 2 million deep it took longer than 1 hour to flatten.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1044
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 31 Dec 2010 12:21:40 +0000 (12:21 +0000)]
Extra assertion. Assert that internally created variables aren't already defined.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1043
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 31 Dec 2010 11:56:09 +0000 (11:56 +0000)]
Small leak fix. Didn't delete the variable introduced in the speedup of r1040
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1042
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 31 Dec 2010 02:40:53 +0000 (02:40 +0000)]
Fix the build. The speedup in the prior checkin needs these too.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1041
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 31 Dec 2010 02:35:05 +0000 (02:35 +0000)]
Speedup. This makes it much faster to create some bvconsts.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1040
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 31 Dec 2010 00:03:20 +0000 (00:03 +0000)]
Disable simplifications when printing back. I disabled the functionality when it was first included in r774. I've no idea why I disabled it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1039
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 21 Dec 2010 12:34:26 +0000 (12:34 +0000)]
Work around occasional hang with -g (when timing out).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1038
e59a4935 -1847-0410-ae03-
e826735625c1
smccam [Sat, 18 Dec 2010 02:32:20 +0000 (02:32 +0000)]
Silence some legitimate warnings about int to pointer casts that would
fail on 64-bit systems by turning them into runtime assertions instead.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1037
e59a4935 -1847-0410-ae03-
e826735625c1
smccam [Sat, 18 Dec 2010 01:23:07 +0000 (01:23 +0000)]
Makefile changes to improve the build of libstp.a. Don't include
Main.or files from MiniSAT, since we don't need them, and they bring
in main() functions and zlib dependencies we don't want. Add a c-api
test to try to keep this from regressing again.
Make it easier to pass -fPIC through to the MiniSAT build.
Clean up some comments and trailing whitespace in Makefiles.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1036
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 15 Dec 2010 07:34:49 +0000 (07:34 +0000)]
Adds a command line configuration option that is saved into a map. So that you can do: --config_va=3 for instance.
This will save va="3" into the config_options map.
I'm intending to use this to allow more options to be controlled from the command line without having the hastle of creating new names for each of them.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1035
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 04:05:49 +0000 (04:05 +0000)]
Enable constant bit Propagation with CNF generation.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1034
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 04:01:45 +0000 (04:01 +0000)]
Reduce the cutover for the advance CNF generator to 2M nodes. Annoyingly much more causes a segfault when memory is exhausted.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1033
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 03:58:28 +0000 (03:58 +0000)]
Enable constant bit propagation by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1032
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 03:48:31 +0000 (03:48 +0000)]
Fix build.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1031
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 03:45:32 +0000 (03:45 +0000)]
Maximally precise transfer functions for constant bit propagation.
I'm still working on the multiplication like ones.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1030
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 02:53:02 +0000 (02:53 +0000)]
No longer default to -m32, causes too many problems
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1029
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 28 Nov 2010 02:45:43 +0000 (02:45 +0000)]
Patch from Markus Groß. Thanks. Here is the description that Markus provided:
1. To fix a missing boost header the src/sat/Makefile has to be fixed
This is mentioned and described here: http://groups.google.com/group/stp-users/browse_thread/thread/
94246a7cf288d57
2. To fix compile errors regarding PRIu64 the src/sat/mtl/IntTypes.h has to be renamed.
Because most osx systems have a case insensitive file system #include <inttypes.h> includes the src/sat/mtl/IntTypes.h and therefore the inttypes.h from the c library is never included.
I renamed the file from IntTypes.h to IntTypesMtl.h.
This fixes the bug reported here: http://groups.google.com/group/stp-users/browse_thread/thread/
c00ab4b90c4ae86a
3. In src/sat/cryptominisat2/ClauseAllocator.h I changed two variable types from uint to uint32_t (otherwise I get: unknown type uint)
4. In src/sat/utils/System.cc
The part ifdef __APPLE__ is missing the memUsedPeak function which leads to an linker error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1028
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 6 Nov 2010 10:14:06 +0000 (10:14 +0000)]
Bugfix. simplifying-minisat failed when abstraction/refinement was turned on. The elminate() function needs to be called.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1026
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 3 Oct 2010 03:42:11 +0000 (03:42 +0000)]
Fix. An optimisation added in r1020 was disabled. This caused the unit tests to fail.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1025
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 1 Oct 2010 14:35:44 +0000 (14:35 +0000)]
Bugfix. Unsigned modulus of zero returned 1, it should return 0.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1023
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 24 Sep 2010 00:32:30 +0000 (00:32 +0000)]
Experimental. Push bvand and bvor through concats.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1022
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 12 Sep 2010 14:21:38 +0000 (14:21 +0000)]
Bugfix. r1018 caused wrong answers. It left out a case needed for booth recoding.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1021
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 12 Sep 2010 13:55:09 +0000 (13:55 +0000)]
Speedup. Add bvconcat normalisation. Break bvconcat apart sometimes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1020
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 12 Sep 2010 13:25:39 +0000 (13:25 +0000)]
Bugfix. The prior checkin cleaned up too much. Sometimes we need false things around.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1019
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 12 Sep 2010 12:36:04 +0000 (12:36 +0000)]
Cleanup. Removes some clauses that must be "false".
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1018
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 12 Sep 2010 12:31:57 +0000 (12:31 +0000)]
Fix. Output the statistics for simplifying minisat.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1017
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 10 Sep 2010 14:43:26 +0000 (14:43 +0000)]
When encoding to CNF via ABC, use the simple mapping if there are more than 10M nodes. This is because currently ABC seems to have a 4GB memory limit internally. So any more than about 10M nodes maxes out the memory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1016
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 8 Sep 2010 02:46:59 +0000 (02:46 +0000)]
Adds a Userflag to control whether the xor solver is enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1015
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 7 Sep 2010 14:21:46 +0000 (14:21 +0000)]
Bugfix to the prior revision. Solving for 2 operand XORs didn't work properly.
Better simplifications. The xor solver now matches negated symbols too. The attached test case now simplifies down.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1014
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 7 Sep 2010 13:09:42 +0000 (13:09 +0000)]
Experimental. Convert IFF to XOR during simplification. This causes XORs of the attached unit test to flatten further.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1013
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 3 Sep 2010 19:11:53 +0000 (19:11 +0000)]
aligned the STP help printout (-h option). It is easier to read now.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1012
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 3 Sep 2010 19:09:47 +0000 (19:09 +0000)]
aligned the STP help printout (-h option). It is easier to read now.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1011
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 31 Aug 2010 14:43:53 +0000 (14:43 +0000)]
Fresh variables created for internal uses, for instance to replace READs during abstraction/refinement. Are now better tracked so that they can be ignored when the model is printed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1010
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 31 Aug 2010 14:07:37 +0000 (14:07 +0000)]
Update the comments to match the last commit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1009
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 31 Aug 2010 13:59:43 +0000 (13:59 +0000)]
Fix to the bvsolver. Some cases were missing when identifying monomials.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1008
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 29 Aug 2010 12:24:44 +0000 (12:24 +0000)]
Bugfix in cbitp. Currently not enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1007
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 28 Aug 2010 13:54:54 +0000 (13:54 +0000)]
Fix error in experimental constant bit propagation code
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1005
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 28 Aug 2010 12:57:55 +0000 (12:57 +0000)]
Bugfix. Memory was sometimes read after it had been freed by the garbage collector
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1004
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 28 Aug 2010 03:01:26 +0000 (03:01 +0000)]
Fix. I thought the code I checked-in just now wasn't active. But it was. This patch adds a flag to disable the prior patch.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1003
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 28 Aug 2010 02:52:36 +0000 (02:52 +0000)]
Changes to inactive by default code.
This patch makes the term-level simplifier, the bit-blaster and the constant bit propagation co-operate during simplification. If the cbitp or the bitblaster discover a new constant. Then the term-level simplifier will be re-ran.
I haven't experimented whether this is useful yet.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1002
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 22 Aug 2010 07:18:30 +0000 (07:18 +0000)]
Remove some assertion checks from code that's not enabled by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1000
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 22 Aug 2010 06:43:22 +0000 (06:43 +0000)]
Bugfix. STP returned the wrong answer when something like bitwidth of 1: (0 = (1+1)) made it to the bitblaster. Simplifying terms collapses (as we do now), collapses this down to (0 =0) which returns the correct answer. The bitvector solver didn't expect to see two constant in a plus.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@998
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 21 Aug 2010 19:57:59 +0000 (19:57 +0000)]
minor changes to INSTALL instructions
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@997
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 20 Aug 2010 12:33:49 +0000 (12:33 +0000)]
Fix the build script
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@996
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 20 Aug 2010 12:18:10 +0000 (12:18 +0000)]
Remove variables from the configure script which controlled the choice of SAT solver
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@995
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 20 Aug 2010 12:15:27 +0000 (12:15 +0000)]
Remove binaries I checked in by mistake
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@994
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 20 Aug 2010 12:10:30 +0000 (12:10 +0000)]
Fix build. Forgot to checkin these
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@993
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 20 Aug 2010 12:07:42 +0000 (12:07 +0000)]
* Replace minisat 2 with minisat 2.2.
* Replace simplifying-minisat 2 with simplifying-minisat 2.2
* It's no longer necessary to compile cryptominisat separately. The choice of solver is controlled by a command line flag now.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@992
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 18 Aug 2010 10:17:37 +0000 (10:17 +0000)]
Add regresssmtcomp2007 which runs the bitvector benchmarks from the 2007 contest
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@991
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 18 Aug 2010 07:25:11 +0000 (07:25 +0000)]
Changes to inactive code. Use simple AIG simplifications on complex problems.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@989
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 16 Aug 2010 03:44:22 +0000 (03:44 +0000)]
Update to currently inactive code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@988
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 16 Aug 2010 01:02:58 +0000 (01:02 +0000)]
Code for AIG rewriting with ABC. This code is not currently enabled by default.
I'll enable it when I understand when it's useful.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@987
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 15 Aug 2010 10:55:18 +0000 (10:55 +0000)]
Extra tests for inactive by-default code
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@986
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 15 Aug 2010 04:57:31 +0000 (04:57 +0000)]
Refactor. Remove unncessary code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@985
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 15 Aug 2010 04:06:33 +0000 (04:06 +0000)]
Change non-enabled code.
This improves the bounds aware multiplication encoding (which is not the default encoding for multiplication).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@984
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 14 Aug 2010 03:44:26 +0000 (03:44 +0000)]
Improvement? FlattenKind now recursively flattens it's children.
I was surprised that it didn't already do this.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@983
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 14 Aug 2010 01:56:11 +0000 (01:56 +0000)]
Should cause not runtime effects.
Add a new multiplication variant that uses bounds discovered during constant bit propagation to more efficiently encode multiplications.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@982
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 13 Aug 2010 06:05:05 +0000 (06:05 +0000)]
Speedup. Reduce the number of times that SortByArith is called. Previously:
* If was explicitly called
* Then it was implicitly called when CreateTerm ran.
* Then it was implicitly called again when CombineLikeTerms called CreateTerm.
Remove an unecessary flatten.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@981
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 Aug 2010 01:27:26 +0000 (01:27 +0000)]
Print out a not yet supported error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@980
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 11 Aug 2010 00:58:57 +0000 (00:58 +0000)]
Add a sorting network implementation. This code is not currently enabled so this patch should do nothing.
Sorting networks should have better propagation (at higher cost) than addition networks (which we currently encode multiplication to).
In my experiments the sorting networks aren't clearly better than the addition networks.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@979
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 10 Aug 2010 05:39:33 +0000 (05:39 +0000)]
Cleanup. Remove experimental (not active) code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@977
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 10 Aug 2010 02:15:32 +0000 (02:15 +0000)]
Improve the encoding of the full adder used by the multiplication circuit.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@974
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 10 Aug 2010 00:41:55 +0000 (00:41 +0000)]
Correct a comment
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@973
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 7 Aug 2010 13:33:28 +0000 (13:33 +0000)]
Bugfix. --output-CNF was broken when outputting with Cryptominisat. A signed / unsigned problem.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@972
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Aug 2010 01:59:14 +0000 (01:59 +0000)]
Fix slowdown.
r965 removed a cache update that caused bitblaster.cvc to run 10 times slower. This update adds back in the cache update as well as changes to ensure that by the end of SimplifyTerm the invariant that actualInput maps to something that hasBeenSimplified(output) holds for.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@968
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 5 Aug 2010 15:17:31 +0000 (15:17 +0000)]
Speedup the bvsolver. Use the applySubstitutionMap function to apply the discovered replacements rather than using simplifyFormula. This means that the simplification caches don't need to be cleaned out (saving time).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@967
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 5 Aug 2010 05:07:06 +0000 (05:07 +0000)]
Bugfix. The prior revision sometimes returned the wrong result (very rarely).
In the prior revision I removed some explicit calls to simplifyTerm.
Wrongly believing that the term was already simplified at the point.
To check that it was simplified I asserted the "hasBeenSimplified" function.
But the hasBeenSimplified function only checked that the term was present in the simplifyMap.
That is that simplifyTerm had been called on it.
Which isn't the same thing as being simplified.
i.e. term A is not simplified if in the SimplifyMap it's mapped to term B.
It's only simplified if A maps to A.
Some simplification functions expect their children to already be simplified.
This wasn't the case so we'd get the wrong answer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@965
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 1 Aug 2010 04:20:59 +0000 (04:20 +0000)]
Bugfix. Infinite loop. My fourth attempt to fix the problem introduced in r947. I've been careful this time.
Refactor. Remove explicit calls to SimplifyTerm if simplify_upfront is enabled. This is a precursor to removing many of the SimplifyTerm calls in the SimplifyTerm function, nearly all are redundant because at the end of the function we have:
if (inputterm != output)
output = SimplifyTerm(output);
i.e. we fixed point it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@964
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 31 Jul 2010 13:26:37 +0000 (13:26 +0000)]
Bugfix. Oops. When using the quick statistics (the -t option), record the time spent generating the CNF.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@963
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Jul 2010 13:23:12 +0000 (13:23 +0000)]
Speedup. I've measured the performance of bit blasted comparisons on a (single) test case. I've selected the fastest encoding.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@962
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Jul 2010 11:53:41 +0000 (11:53 +0000)]
Bugfix. Infinite loop. A third fix for r947.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@960
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Jul 2010 07:01:58 +0000 (07:01 +0000)]
Bugfix. STP may produce the wrong answer. Introduced revision 947.
I enabled creation of multiplication nodes with >2 children. But the DistributeMultOverPlus function ignores the third (and later) children.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@958
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Jul 2010 03:09:57 +0000 (03:09 +0000)]
Speed up of the unsigned division encoding. Update the runtimes for the different variants of unsigned division.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@957
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Jul 2010 02:05:38 +0000 (02:05 +0000)]
Refactoring.
* CreateSymbol now takes the indexWidth and the valueWidth.
* I've removed most of the calls to setIndexWidth.
* CreateSymbol has been moved into the NodeFactory class.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@956
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 26 Jul 2010 23:26:50 +0000 (23:26 +0000)]
Bugfix. Stop a null pointer error.
The simplifier can create something like: (BVMULT 1 3 5). i.e. a mutliplication node of constants with arity > 2. This patch makes that work.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@954
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 26 Jul 2010 12:21:20 +0000 (12:21 +0000)]
Further fixing of spurious printing in CryptoMiniSat
As per report by Trevor Hansen
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@953
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 26 Jul 2010 12:17:44 +0000 (12:17 +0000)]
Fixing verbosity-related problems in CryptoMiniSat2
Reported by Trevor Hansen
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@952
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 14:49:13 +0000 (14:49 +0000)]
A QF_ABV division has been added to the smt-lib. Update parser to read, update printer to write it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@951
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 14:24:13 +0000 (14:24 +0000)]
Bugfix. Properly print out the counter example of booleans.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@950
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 09:55:19 +0000 (09:55 +0000)]
Fix the build + extra options for constant bit propagation (not currently enabled).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@949
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 09:46:47 +0000 (09:46 +0000)]
Speedup. Flatten multiplications, sort, then re-assable into 2-arity functions. This detects some associativity.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@947
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 09:45:19 +0000 (09:45 +0000)]
Extra code (not enabled), for constant bit propagation.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@946
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 09:43:33 +0000 (09:43 +0000)]
Extra code (that's not currently enabled), so reduce the unncessary clearing of the simplification map during bit-vector solving. This patch causes some instances to fail.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@945
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 10 Jul 2010 04:54:09 +0000 (04:54 +0000)]
Output quick statistics if enabled, and exiting after generating the CNF.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@944
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 9 Jul 2010 14:06:23 +0000 (14:06 +0000)]
Decision. This optimisation helps our cvc regressions but hurts our smtlib ones. So I'm taking it out..
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@943
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 9 Jul 2010 08:28:46 +0000 (08:28 +0000)]
Add the option to exit after generating the CNF. Currently only works for bit-vectors (which don't have abstraction refinement).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@942
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 9 Jul 2010 08:25:48 +0000 (08:25 +0000)]
Bugfix. If a new-line occured in a string literal, it wasn't matched by the lexer, so would be printed out to the console.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@941
e59a4935 -1847-0410-ae03-
e826735625c1
petercol [Thu, 8 Jul 2010 17:12:36 +0000 (17:12 +0000)]
Introduce vc_setInterfaceFlags function
This patch adds a vc_setInterfaceFlags function to the C interface
with one possible flag, EXPRDELETE, which is set by default. The flag
controls whether the C interface deletes types and integer constant
expressions at vc_Destroy time. It is intended that clients which
perform their own memory management of these objects will be able to
clear this flag.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@940
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:16:17 +0000 (05:16 +0000)]
Fix some small leaks when performing division by zero, and in the smtlib1 parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@939
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:14:38 +0000 (05:14 +0000)]
Only run the bvsolver if optimisations have been enabled. The bvsolver relies on optimisations being performed for correctness.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@938
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:10:55 +0000 (05:10 +0000)]
Fix the unit test script:
* To not explicitly call simplifying minisat (which isn't an option if compiled with cms).
* To remove comments and blank lines (which are introduced by AIG's conversion).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@937
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 13:33:08 +0000 (13:33 +0000)]
Bugfix. Remove a null pointer reference.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@936
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 13:17:57 +0000 (13:17 +0000)]
Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.
Other changes are for constant bit propagation (aren't active yet).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@935
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:51:08 +0000 (07:51 +0000)]
Fix the building of the stp library.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@934
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:37:55 +0000 (07:37 +0000)]
Fix the build.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@933
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:33:58 +0000 (07:33 +0000)]
Neaten up the code for constant bit propagation. Note this code doesn't run by default, so this patch shouldn't change anything.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@932
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 14:38:52 +0000 (14:38 +0000)]
Bugfix. Fix a check to ensure that the type of nodes doesn't change for the worst.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@931
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log