Improvement. Only create possible values if it can help.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1183 e59a4935-1847-0410-ae03-e826735625c1

Enable ITE Context stuff by default.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1182 e59a4935-1847-0410-ae03-e826735625c1

Refactor. I experimented with changing the allocator used when parsing. But, it didn't make any measurable difference in the time taken.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1181 e59a4935-1847-0410-ae03-e826735625c1

Improvement. Add an equality simplification.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1180 e59a4935-1847-0410-ae03-e826735625c1

Improvement. Enable ITE context simplifications again.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1179 e59a4935-1847-0410-ae03-e826735625c1

Disable ITE context simplifications. It's too slow on some CVC test cases to justify it.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1178 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Terrible. Forgot to delete debugging code. Too late.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1177 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Terrible. The last checkin causes STP to sometimes return the wrong answer I suspect.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1176 e59a4935-1847-0410-ae03-e826735625c1

Improvement. An analysis that simplifies ITES by determining what must be true/false down each branch.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1175 e59a4935-1847-0410-ae03-e826735625c1

No semantic change. Fix a mistake that caused no effect.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1172 e59a4935-1847-0410-ae03-e826735625c1

Fix.  XORs with >2 children sometimes reached the simplifier. This patch adds simplification for those, rather than generating an assertion error.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1171 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Terrible! Another fix. STP r1149 to here will sometimes return the wrong answer.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1170 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Terrible! STP r1149 to here will sometimes return the wrong answer. I was wrong about the semantics of .insert(..), I thought it replaced the new value if it was already present.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1169 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. The prior checkin added an assertion that didn't always hold.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1168 e59a4935-1847-0410-ae03-e826735625c1

Finish refactoring of the ArrayTransformer class.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1167 e59a4935-1847-0410-ae03-e826735625c1

Partial refactor. Remove the Arrayread_SymbolMap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1166 e59a4935-1847-0410-ae03-e826735625c1

Partial refactor. Removing the Arrayname_ReadindicesMap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1165 e59a4935-1847-0410-ae03-e826735625c1

Partial refactoring. Removing the arrayread_itemap.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1164 e59a4935-1847-0410-ae03-e826735625c1

Refactoring.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1163 e59a4935-1847-0410-ae03-e826735625c1

Bugfix. Fix the prior checkin.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1162 e59a4935-1847-0410-ae03-e826735625c1

Partial Refactor. I'm reducing the number of collections in the ArrayTransformer class, but it's causing difficult to find defects. This adds a new collection. I'll remove the old ones later.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1161 e59a4935-1847-0410-ae03-e826735625c1

Extra test cases that should be simplified down to nothing.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1160 e59a4935-1847-0410-ae03-e826735625c1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

* 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

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

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

 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

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

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

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

* 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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