]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Wed, 26 Jan 2011 00:04:43 +0000 (00:04 +0000)]
Speedup. Problems with lots of pluses sometimes ran slowly. For the same reason that BVOR/BVAND ones did.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1091
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 26 Jan 2011 00:03:25 +0000 (00:03 +0000)]
Fix. The c-api wasn't working because refactored object files were missing.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1090
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 Jan 2011 14:28:17 +0000 (14:28 +0000)]
Fix. Ooops. I'd commented out the fix of r1082 / r1083.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1089
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 Jan 2011 13:08:12 +0000 (13:08 +0000)]
Refactor. Move the code that goes to CNF via ASTNodes to it's own directory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1087
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 Jan 2011 12:52:36 +0000 (12:52 +0000)]
Refactor. Move the clause bucket size so it can be adjusted at runtime.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1086
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 Jan 2011 00:57:04 +0000 (00:57 +0000)]
Bugfix. An assertion error would be produced because a term was not simplified.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1082
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 06:03:03 +0000 (06:03 +0000)]
Fix. remove the -j option. Which did nothing. It used to output a CNF from the contents of cryptominisat's insides. Not from the other solvers.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1081
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 05:28:27 +0000 (05:28 +0000)]
Fix. sat, unsat, unknown aren't reserved words so they can be used as variable names in the SMTLIB2 format. Treat them instead as strings.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1080
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 04:52:39 +0000 (04:52 +0000)]
The gulwani smtlib tests require arity > 2 bvplus and bvmult. It's not part of the specification, but it's easy to include...
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1078
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 04:06:24 +0000 (04:06 +0000)]
Speedup. When parsing don't create symbols for the let names. Use strings instead.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1076
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 01:29:22 +0000 (01:29 +0000)]
Cleanup / Refactor. Will call the sat solver fewer times.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1075
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 01:05:12 +0000 (01:05 +0000)]
Bugfix. Maybe. Empty smtlib and smtlib2 format files would cause a segfault / bad thing. I suspect these should be allowed, but haven't checked versus the specification.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1073
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 19 Jan 2011 00:32:46 +0000 (00:32 +0000)]
Add the --config_full_bvsolve=1 option. With this option enabled, I know of no other segfaults/crashes in STP. However, for now, enabling it causes STP to run very slowly when processing problems with arrays.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1071
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 18 Jan 2011 12:51:49 +0000 (12:51 +0000)]
Fix. ClearAllTables() deleted all the dynamically allocated memory, but left the containers that pointed to them around. Fine if called by the destructor, not fine if called elsewhere.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1070
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 18 Jan 2011 12:45:56 +0000 (12:45 +0000)]
Bugfix. The same index could be stored twice in the array. I suspect it used to cause problems. But don't have any fixed test cases to prove it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1069
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 18 Jan 2011 12:39:03 +0000 (12:39 +0000)]
Cleanup. Scope a variable so that it's killed of early.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1068
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 18 Jan 2011 12:35:57 +0000 (12:35 +0000)]
Bugfix. Experimental. Complicated input caused an assertion failure. Switching this option is the easy way to fix it. I'm not sure this is the right thing to do.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1066
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 17 Jan 2011 11:21:46 +0000 (11:21 +0000)]
Speedup. Use the better caching for the bit-vector solver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1065
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 14 Jan 2011 23:35:48 +0000 (23:35 +0000)]
Bugfix. Running with -t would fail if the shortcut was taken.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1064
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 13 Jan 2011 12:54:12 +0000 (12:54 +0000)]
Remove experimental code (that wasn't enabled). That doesn't help.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1063
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 13 Jan 2011 02:08:43 +0000 (02:08 +0000)]
Bugfix. I forgot the return on a function. This only caused a problem if STP tried to return a wrong answer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1062
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 9 Jan 2011 15:31:18 +0000 (15:31 +0000)]
Bugfix. Another leak introduced in r1055.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1061
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 9 Jan 2011 11:04:02 +0000 (11:04 +0000)]
Bugfix. A large memory leak was introduced in r1055.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1060
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 9 Jan 2011 04:05:09 +0000 (04:05 +0000)]
Fix a small memory leak.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1059
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 9 Jan 2011 04:04:12 +0000 (04:04 +0000)]
Fix small memory leak.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1058
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 8 Jan 2011 04:23:57 +0000 (04:23 +0000)]
Bugfix to the incremental cnf code (which isn't yet active).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1057
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 8 Jan 2011 04:10:57 +0000 (04:10 +0000)]
Allow incremental building of the CNF from AIGs using Tseitin.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1056
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 8 Jan 2011 03:53:36 +0000 (03:53 +0000)]
* Speed up the bvsolver. Reduce the number of copies of sets by storing pointers in a map.
* Refactor the constant evaluator. Give a function that removes the need to first create the node that's been processed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1055
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 7 Jan 2011 11:58:49 +0000 (11:58 +0000)]
Cleanup/Speedup. Minor changes to simplify formula.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1054
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 6 Jan 2011 00:11:41 +0000 (00:11 +0000)]
Bugfix. Would segfault if a vector was empty.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1053
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 3 Jan 2011 05:11:54 +0000 (05:11 +0000)]
* Remove the arraywrite_refinement_flag boolean flag. It didn't seem to do anything.
* If refinement is turned off, then use the AIG CNF conversion code (which is much much better).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1052
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 3 Jan 2011 02:48:52 +0000 (02:48 +0000)]
Speedup, Cleanup of the SATBased_ArrayReadRefinement. It did lots of unnecessary work
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1051
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 2 Jan 2011 13:42:22 +0000 (13:42 +0000)]
Bugfix. Prevent *TrueDummy* being output in the counter example.
This is a nicer way of stopping it being output.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1050
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 2 Jan 2011 12:08:03 +0000 (12:08 +0000)]
Speedup. Experimental. Caching was disabled when converting a term to a constant using the model, IF the arrayReadFlag was false. Without caching it runs very slowly when building the counter example.
I've yet to find an instance where caching all the time gives the wrong example??
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1049
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 2 Jan 2011 12:03:38 +0000 (12:03 +0000)]
Refactor. Remove some commented out code. No idea what it did.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1048
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log