]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Tue, 22 Feb 2011 11:44:12 +0000 (11:44 +0000)]
Refactor. Overcome a temporary static fetish. Now better.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1159
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 11:34:18 +0000 (11:34 +0000)]
Improvement. Match the difficulty score better to the number of AIG nodes created.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1158
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 00:19:08 +0000 (00:19 +0000)]
Improvement. The start of an unsigned interval simplification.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1157
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 22 Feb 2011 00:16:17 +0000 (00:16 +0000)]
Improvement. Handle extracts especially when doing unconstrained variable elimination.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1156
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 06:14:33 +0000 (06:14 +0000)]
Bugfix. r1152 was broken. It got the widths wrong.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1154
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 04:26:59 +0000 (04:26 +0000)]
A new test case for the special unconstrained extract handling.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1153
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Feb 2011 04:06:29 +0000 (04:06 +0000)]
Improvement. Simplifying EQ a little better.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1152
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:23:43 +0000 (01:23 +0000)]
Add find pure literals code.oooops.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1149
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:22:10 +0000 (01:22 +0000)]
Enable pure literal elimination, and unconstrained variable elimination by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1148
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:15:57 +0000 (01:15 +0000)]
Remove unused configuration option. Update qualifiers.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1147
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:14:05 +0000 (01:14 +0000)]
Add --config options to enable CNF conversion via Tseitin, and AIG rewrites.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1146
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:11:30 +0000 (01:11 +0000)]
Add the code for unconstrained variable elimination. This is not currently enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1145
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Feb 2011 01:01:57 +0000 (01:01 +0000)]
Improvements.
* Add a function to update the substitution map that avoids the expensive checks. This is used by unconstrained variable elimination.
* use a --config flag to enable the xor solver.
* Update the dependencies with functions for unconstrained elimination.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1144
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Feb 2011 00:43:00 +0000 (00:43 +0000)]
Add categories to the RunTime class for new simplifications
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1143
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Feb 2011 06:57:44 +0000 (06:57 +0000)]
Fix a leak in _asserts. I know of no other leaks.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1141
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Feb 2011 05:48:48 +0000 (05:48 +0000)]
Improvement. The SMTLIB1 & SMTLIB2 parsers were holding references to nodes when they didn't need to.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1140
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:59:06 +0000 (01:59 +0000)]
Add conditional workaround for flex < 2.5.20, such as in RedHat.
- Old versions of flex did not support the -f flag, and did not provide a destroy function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1139
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:59:02 +0000 (01:59 +0000)]
Clean up the build system for src/parser.
- Rename files consistently to be usable in pattern rules, and use patterns rules for flex/bison.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1138
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:58:51 +0000 (01:58 +0000)]
Temporarily rename CVC.* to cvclib.*; to be renamed in the next patch to cvc.* (workaround to handle case-only renames).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1137
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:31:59 +0000 (01:31 +0000)]
Fix inconsistent line endings, and execute bit on a couple of .sh files (so that SVN with eol-style/mime-type auto-props won't complain).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1136
e59a4935 -1847-0410-ae03-
e826735625c1
khooyp [Thu, 10 Feb 2011 01:21:54 +0000 (01:21 +0000)]
Fix a typo in the help string.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1135
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 14:35:17 +0000 (14:35 +0000)]
Fix. For r1131 I deleted the wrong file.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1133
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:17:21 +0000 (13:17 +0000)]
Patch from Khoo Yit Phang.
Delete several files to address "ranlib: ... has no symbols" warnings (they actually are completely empty).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1132
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:13:04 +0000 (13:13 +0000)]
Patch from Khoo Yit Phang.
Remove extlib-abc/vecAtt.h to eliminate warnings (it's unused anyway).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1131
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 13:08:40 +0000 (13:08 +0000)]
Patch from Khoo Yit Phang.
Fix typo for FreeBSD (untested).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1130
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:29:21 +0000 (12:29 +0000)]
Patch from Khoo Yit Phang.
Fix the weird type of STPMgr::CreateBVConst (to have only one reference level).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1129
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:22:10 +0000 (12:22 +0000)]
Patch from Khoo Yit Phang.
Add a workaround for GCC 4.0 which doesn't extend friendship to nested classes.
See http://stackoverflow.com/questions/
3584385 /friend-access-to-protected-nested-class for details.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1128
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:20:23 +0000 (12:20 +0000)]
Patch from Khoo Yit Phang.
Clean up scripts/configure, and add flags to set CC and -fpic.
- Use POSIX shell parameter expansion when parsing flags, instead of expr.
- Fix the test for $CC/$CXX to work when they contain spaces (e.g., "gcc -m32").
- Export flags in config.info to ensure that the entire build, including recursive Makefiles, consistently use the given flags.
- Don't create the installation directories when configuring; do it when installing.
- Remove minisat configuration flags from scripts/configure, since they are unused.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1127
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:18:01 +0000 (12:18 +0000)]
Patch from Khoo Yit Phang.
General clean-up of the build system.
- Remove unused or unnecessary flags and rules.
- Fix up automatic dependency generation.
- Move final linking of bin/stp to the topmost Makefile for better dependency control.
- Update versionString.cpp only if the version changed, to avoid unnecessary rebuild.
- Build src/sat/libminisat.a and lib/libstp.a by concatenating their constituent archives, rather than by relisting their contained object files.
- Add dependencies for bin/stp and lib/libstp.a to rebuild them only when necessary.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1126
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 12:00:08 +0000 (12:00 +0000)]
Patch from Khoo Yit Phang.
Drop support for building universal binaries on OS X, since it raises rather annoying build issues.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1125
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:51:42 +0000 (11:51 +0000)]
Patch from Khoo Yit Phang.
uRemove -I../AST from CFLAGS, and change all affected #include to use relative paths.
This is in preparation to fix up automatic dependencies generation to use "gcc -MG" to handle the generated
src/AST/ASTKind.h file, which works more reliably when #include uses relative paths.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1124
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:48:30 +0000 (11:48 +0000)]
Patch from Khoo Yit Phang.
Clean up the build system of MiniSat.
- Set up dependencies for recursive Makefile to avoid unnecessary rebuilds.
- Correctly propagate configuration to recursive Makefiles by exporting flags and removing unnecessary rules.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1123
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Feb 2011 11:41:47 +0000 (11:41 +0000)]
Patch from Khoo Yit Phang. Fix typos that caused main() to be linked into MiniSat's libraries.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1122
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Feb 2011 14:05:30 +0000 (14:05 +0000)]
Speedup the test harness. For the CVC tests STP is taking about 200 seconds, and the harness about 60.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1121
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Feb 2011 14:04:31 +0000 (14:04 +0000)]
Improvement. Simplifiy from (X bvdiv 1) to X.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1120
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Feb 2011 01:34:36 +0000 (01:34 +0000)]
Speedup. When performing constant bit propagation, there is now a slow & a fast worklist. The cheap propagators in the slow worklist are called first.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1119
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 04:00:54 +0000 (04:00 +0000)]
Improvement. Reduce the scope of the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1118
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 03:47:13 +0000 (03:47 +0000)]
Convert these tests from cvc to smtlib2 format. The model seems to contain a division by zero. The currently implementation of the CVC language treats that as bad. It probably shouldn't, but I don't want to change the semantics. However, division by zero is defined in smtlib2. So I've converted them.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1117
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Feb 2011 01:57:49 +0000 (01:57 +0000)]
Bugfix. The c-api calls ~STP and ~STPMgr. The changes I made to the destructors in r1115 broke the c-api.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1116
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 12:32:36 +0000 (12:32 +0000)]
Improvement. Cleanup memory better at the end.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1115
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 05:39:54 +0000 (05:39 +0000)]
Improvement. Use ABC's CNF converter by default when solving array problems using minisat.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1114
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 03:10:05 +0000 (03:10 +0000)]
Remove no longer used code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1113
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 2 Feb 2011 00:55:06 +0000 (00:55 +0000)]
Fix. Apply substitutions in another place to avoid an assertion error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1112
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Feb 2011 12:41:57 +0000 (12:41 +0000)]
Less Memory. Cache less frequently.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1111
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 1 Feb 2011 12:40:57 +0000 (12:40 +0000)]
Speedup. Track which sets have already being added to a cache, and don't add them again.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1110
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 31 Jan 2011 14:12:12 +0000 (14:12 +0000)]
Fix. Without a CallSAT_Result check call sometimes we get the wrong result. No idea why yet.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1109
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 31 Jan 2011 14:06:53 +0000 (14:06 +0000)]
Fix. If not simplifying during parsing an assertion was violated.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1108
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:26:06 +0000 (13:26 +0000)]
Bugfix. Substitutions need to be written through arrays too. 2/2.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1103
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:13:17 +0000 (13:13 +0000)]
Bugfix. Substitutions need to be written through arrays too.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1101
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 13:11:58 +0000 (13:11 +0000)]
* The -t option now tracks time spent applying the substitution map.
* Some functions that should be private in the SubstitutionMap were made private.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1100
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 12:45:32 +0000 (12:45 +0000)]
Fix. The last revision has some debugging messages enabled. Ooops.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1099
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 05:44:01 +0000 (05:44 +0000)]
Improvement. Add substitution for variables by arbitary terms when creating substitution maps. The difficult part is check that substitutions don't create loops. This code replaces the old --config_full_bvsolve=1 option.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1098
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 Jan 2011 02:26:28 +0000 (02:26 +0000)]
Remove the full bvsolve option. I'm soon to commit a much better replacement of this.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1097
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 Jan 2011 07:06:19 +0000 (07:06 +0000)]
Cleanup. Remove Doug Lea's Malloc which is no longer used. We used to use dl malloc to give minisat a region of memory to allocate its data structures in. This meant that they were all close together in memory so that when cache line were stored, the lines would more often contain minisat data, rather than STP's data. However, Minisat 2.2 has a better allocator, so it allocates more of its stuff together in memory. The difference between the embedded minisat 2.2 in STP, and running it from the command line, is about 4%. Not a large enough difference to worry about.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1096
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 Jan 2011 06:28:11 +0000 (06:28 +0000)]
Improvement. Output peak memory usage, and CPU time used when using the -t option.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1095
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 Jan 2011 02:38:19 +0000 (02:38 +0000)]
Refactor. Split out the code to determine which variables are contained in an expression.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1094
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 26 Jan 2011 23:33:34 +0000 (23:33 +0000)]
* Improvement. Add array read refinement to the quick statistics.
* Speedup. Cache more things when doing array read refinement.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1093
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 26 Jan 2011 05:01:53 +0000 (05:01 +0000)]
Fix. Thanks to Dan Kaminsky for the report. It didn't compile on gcc 4.1.2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1092
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log