]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Wed, 23 Mar 2011 03:13:08 +0000 (03:13 +0000)]
Refactor. Changes to whitespace only.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1227
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Mar 2011 02:21:13 +0000 (02:21 +0000)]
Refactor. A new function to check if there are unapplied variable substitutions.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1226
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Mar 2011 00:28:45 +0000 (00:28 +0000)]
Now assume there will be no unapplied substitutions when unconstrained variable elimination starts.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1225
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Mar 2011 00:19:46 +0000 (00:19 +0000)]
Refactor. Convert from if-then-else to a switch.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1224
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Mar 2011 06:47:55 +0000 (06:47 +0000)]
Adds extra cases to the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1223
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 21 Mar 2011 03:59:42 +0000 (03:59 +0000)]
Fix division by zero results. x % 0, now equals x.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1222
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Mar 2011 04:05:24 +0000 (04:05 +0000)]
Fix. x bvmod 0, now evaluates to x, not to 0.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1221
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Mar 2011 02:36:09 +0000 (02:36 +0000)]
Improvement. More cases for the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1220
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Mar 2011 13:27:41 +0000 (13:27 +0000)]
Remove debugging printf.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1219
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Mar 2011 12:32:07 +0000 (12:32 +0000)]
Test case for r1217.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1218
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Mar 2011 12:30:31 +0000 (12:30 +0000)]
Improvement. Pull bvsx through multiplication, signed division and plus.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1217
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Mar 2011 00:16:20 +0000 (00:16 +0000)]
Improvement. Add more operations to the unsigned interval analysis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1216
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Mar 2011 00:22:01 +0000 (00:22 +0000)]
Improved unsigned interval analysis. Extra operations are added. It now re-writes signed operations to unsigned if the sign bit is fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1215
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 16 Mar 2011 13:58:56 +0000 (13:58 +0000)]
Add some extra simplifications to the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1214
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Mar 2011 03:57:45 +0000 (03:57 +0000)]
* The simplifying node factory now removes TRUEs when creating ANDS.
* The simplifying node factory never creates IFF, just XORS.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1213
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Mar 2011 03:38:14 +0000 (03:38 +0000)]
Improvement. Start to use the simplifying node factory in the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1212
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Mar 2011 02:59:02 +0000 (02:59 +0000)]
Improvement. With stats enabled, only output the first unique config_ option found.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1211
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Mar 2011 02:30:22 +0000 (02:30 +0000)]
Make SimplifyFormula idempotent. I don't know if this is quicker.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1210
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Mar 2011 00:46:02 +0000 (00:46 +0000)]
Experimental. Simplify all the bit-vector children before simplifying the term. Conceptually this is better, but I don't know if it's faster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1209
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 23:24:15 +0000 (23:24 +0000)]
Improvement. Add a simple read over write simplification to the simplifying node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1208
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 13:30:23 +0000 (13:30 +0000)]
* Clean up the simplifier some.
* Add times for the basic interval analysis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1207
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 04:19:20 +0000 (04:19 +0000)]
Refactor. Remove the simplify_upfront option. It's now hardcoded.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1206
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Mar 2011 04:09:22 +0000 (04:09 +0000)]
Refactor. Remove code that's not used.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1205
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 23:36:07 +0000 (23:36 +0000)]
Fix. Missing break; in a switch. Dumb luck meant it didn't cause any problems.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1204
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:49:33 +0000 (12:49 +0000)]
Fix. r1201 added a message to cout.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1203
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:28:33 +0000 (12:28 +0000)]
Improvement. Add a size reducing phase prior to performing simplifications that may increase the size of the problem. If the the DAG gets bigger by some amount, then we revert back to the saved copy of the problem.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1202
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 12:13:26 +0000 (12:13 +0000)]
Improvements.
* The BVSolver doesn't necessarily apply the simplify..() functions (which can increase the DAGs size).
* Unsimplified input doesn't cause it to fail.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1201
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Mar 2011 11:42:58 +0000 (11:42 +0000)]
Fix. This assert() was very slow sometimes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1200
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 14:35:13 +0000 (14:35 +0000)]
Bugfix. r1194 didn't preserve the doubly linked list.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1199
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 05:12:44 +0000 (05:12 +0000)]
Fiddle with the difficulty scorer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1198
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 10 Mar 2011 02:01:49 +0000 (02:01 +0000)]
Fiddle with the difficulty scorer to better estimate how hard the problem becomes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1197
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 06:42:07 +0000 (06:42 +0000)]
Miscellaneous improvements.
* Use the simplifying node factory in more places.
* If simplifications are turned off, don't simplify in the transformer.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1196
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 04:14:36 +0000 (04:14 +0000)]
Fix. In the prior checkin I didn't keep track of which nodes had been visited.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1195
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Mar 2011 03:45:26 +0000 (03:45 +0000)]
Improvement. Now do unconstrained elimination for all inequalities.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1194
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Mar 2011 12:18:54 +0000 (12:18 +0000)]
Extra simplification rules for BVAND, and EQ. These sometimes make one of the grep big-array tests use 2.5GB of RAM during solving.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1193
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 7 Mar 2011 02:48:14 +0000 (02:48 +0000)]
Improvement. Add an extra simplification rule for BVDIV/ BVMOD.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1192
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 6 Mar 2011 23:15:48 +0000 (23:15 +0000)]
Add simplification of the top-most propositional part of the problem using AIGs. This is currently disabled by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1191
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 11:57:10 +0000 (11:57 +0000)]
improvement. Use the simplifying node factory be default in the substitution map.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1190
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:23:46 +0000 (03:23 +0000)]
Tiny improvement. Create slightly fewer nodes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1189
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:21:07 +0000 (03:21 +0000)]
Fix a leak. I'd forgotten to call fclose().
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1188
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 5 Mar 2011 03:14:50 +0000 (03:14 +0000)]
Fix a leak introduced in r1184.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1187
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 12:44:08 +0000 (12:44 +0000)]
Improvement. Specialise the replace function more for replacing symbols by other things. This is considerably faster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1186
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 06:12:23 +0000 (06:12 +0000)]
Refactor. Neaten up the CreateSubstitutionMap function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1185
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 06:03:24 +0000 (06:03 +0000)]
Fixes / Improvements.
* Fix. No longer create NOT(NOT(..)) nodes because their node numbers aren't unique.
* Improvement. Change the AlwaysTrueFormMap (which was a set), to use node numbers ---which allows the nodes to be garbage collected.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1184
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 3 Mar 2011 03:51:48 +0000 (03:51 +0000)]
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
trevor_hansen [Thu, 3 Mar 2011 03:46:53 +0000 (03:46 +0000)]
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
trevor_hansen [Thu, 3 Mar 2011 01:32:14 +0000 (01:32 +0000)]
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
trevor_hansen [Tue, 1 Mar 2011 12:30:42 +0000 (12:30 +0000)]
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
trevor_hansen [Mon, 28 Feb 2011 13:31:43 +0000 (13:31 +0000)]
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
trevor_hansen [Sun, 27 Feb 2011 13:43:44 +0000 (13:43 +0000)]
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
trevor_hansen [Sun, 27 Feb 2011 13:33:16 +0000 (13:33 +0000)]
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
trevor_hansen [Sun, 27 Feb 2011 13:28:39 +0000 (13:28 +0000)]
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
trevor_hansen [Sun, 27 Feb 2011 11:04:04 +0000 (11:04 +0000)]
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
trevor_hansen [Sat, 26 Feb 2011 05:14:40 +0000 (05:14 +0000)]
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
trevor_hansen [Sat, 26 Feb 2011 05:06:58 +0000 (05:06 +0000)]
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
trevor_hansen [Sat, 26 Feb 2011 03:56:39 +0000 (03:56 +0000)]
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
trevor_hansen [Sat, 26 Feb 2011 02:54:10 +0000 (02:54 +0000)]
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
trevor_hansen [Thu, 24 Feb 2011 02:00:15 +0000 (02:00 +0000)]
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
trevor_hansen [Thu, 24 Feb 2011 01:42:37 +0000 (01:42 +0000)]
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
trevor_hansen [Thu, 24 Feb 2011 01:15:57 +0000 (01:15 +0000)]
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
trevor_hansen [Thu, 24 Feb 2011 01:02:33 +0000 (01:02 +0000)]
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
trevor_hansen [Thu, 24 Feb 2011 00:46:48 +0000 (00:46 +0000)]
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
trevor_hansen [Wed, 23 Feb 2011 14:54:22 +0000 (14:54 +0000)]
Refactoring.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1163
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Feb 2011 14:11:31 +0000 (14:11 +0000)]
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
trevor_hansen [Wed, 23 Feb 2011 13:43:18 +0000 (13:43 +0000)]
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
trevor_hansen [Wed, 23 Feb 2011 07:09:20 +0000 (07:09 +0000)]
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
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
projects / francis / stp.git / log