git.unchartedbackwaters.co.uk Git

trevor_hansen [Wed, 13 Apr 2011 01:43:16 +0000 (01:43 +0000)]

Extra simplification rule.

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Apr 2011 15:11:08 +0000 (15:11 +0000)]

oops. Meant to add this too.

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Apr 2011 15:09:31 +0000 (15:09 +0000)]

Add an extra simplification rule to the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Apr 2011 13:26:53 +0000 (13:26 +0000)]

Move some division be zero code into the bitblaster. I'm trying to make the array transformer (which also transforms signed div/mod) idempotent.

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

commit | commitdiff | tree

trevor_hansen [Sun, 10 Apr 2011 11:37:02 +0000 (11:37 +0000)]

Adds code, that's not currently enabled, to read-out all the nodes that the bitblaster discovers should be constant.

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

commit | commitdiff | tree

trevor_hansen [Sun, 10 Apr 2011 04:13:22 +0000 (04:13 +0000)]

Improvement. Use the simplifying node factory in transformer.

This is a hopefully correct implementation of r1260.

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

commit | commitdiff | tree

trevor_hansen [Sun, 10 Apr 2011 03:53:14 +0000 (03:53 +0000)]

Revert the previous revision. It broke lots.

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

commit | commitdiff | tree

trevor_hansen [Fri, 8 Apr 2011 14:57:20 +0000 (14:57 +0000)]

Improvement. Use the simplifying node factory in transformer.

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

commit | commitdiff | tree

trevor_hansen [Fri, 8 Apr 2011 04:33:28 +0000 (04:33 +0000)]

Improvement. Don't add NOT FALSE at the end of the input..

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 14:36:10 +0000 (14:36 +0000)]

Improvement. When a node is simplified set a value so that we can avoid simplifying it later.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 13:43:19 +0000 (13:43 +0000)]

Improvement. Output the time spent in a stage with -s.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 13:38:52 +0000 (13:38 +0000)]

Hack. The ITE context simplification blows out ff.stp, i.e. it takes > 5 minutes. This limits ITE context simplifications to small contexts.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 13:36:23 +0000 (13:36 +0000)]

Revert. I didn't mean to checkin all those changes.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Apr 2011 13:22:05 +0000 (13:22 +0000)]

commit | commitdiff | tree

trevor_hansen [Wed, 6 Apr 2011 03:42:57 +0000 (03:42 +0000)]

Remove junk.

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

commit | commitdiff | tree

trevor_hansen [Wed, 6 Apr 2011 03:42:07 +0000 (03:42 +0000)]

Improve the bvsolver.If the substitution of a monomial fails, then the bvsolver will loop looking for more candidates.

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

commit | commitdiff | tree

trevor_hansen [Wed, 6 Apr 2011 02:59:50 +0000 (02:59 +0000)]

Refactor. Remove junk.

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

commit | commitdiff | tree

trevor_hansen [Sun, 3 Apr 2011 14:14:56 +0000 (14:14 +0000)]

Improvement. Some extra simplifications for the simplifyingNF.

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

commit | commitdiff | tree

trevor_hansen [Sun, 3 Apr 2011 09:49:09 +0000 (09:49 +0000)]

Improvement. The simplifying node factory never creates x + y = y + 2 (say). Instead it removes terms that are common on both sides. Creating x = 2.

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

commit | commitdiff | tree

trevor_hansen [Thu, 31 Mar 2011 13:02:27 +0000 (13:02 +0000)]

Tiny improvement. Add the one-bit operations that evaluate to a child or a constant.

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

commit | commitdiff | tree

trevor_hansen [Thu, 31 Mar 2011 12:39:46 +0000 (12:39 +0000)]

Small improvement. Discard the inner write if the two WRITEs are to the same index.

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

commit | commitdiff | tree

trevor_hansen [Tue, 29 Mar 2011 13:18:23 +0000 (13:18 +0000)]

Work around rare problem caused by the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Mar 2011 03:49:09 +0000 (03:49 +0000)]

Make applySubstitutionMap idempotent (I hope).

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Mar 2011 03:47:25 +0000 (03:47 +0000)]

Improvement. The simplifying node factory now eliminates extract over extracts, as well as some extract over concats.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Mar 2011 00:36:48 +0000 (00:36 +0000)]

During the size reducing transformations, now set the top node to true during constant bit propagation.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Mar 2011 00:35:17 +0000 (00:35 +0000)]

Change the names for some statistics.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Mar 2011 00:34:44 +0000 (00:34 +0000)]

Extra simplification rule for BVXOR.

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

commit | commitdiff | tree

trevor_hansen [Sun, 27 Mar 2011 00:43:13 +0000 (00:43 +0000)]

Add experimental code (not presently enabled), that replaces known values with concatenations.

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

commit | commitdiff | tree

trevor_hansen [Sat, 26 Mar 2011 03:58:20 +0000 (03:58 +0000)]

Improvement. The simplifying node factory no longer creates greater than equal nodes.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Mar 2011 13:34:55 +0000 (13:34 +0000)]

Improvement. Convert left/right (NOT aritmetic), shifts by a known amount to a concatenation and extract in the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Mar 2011 11:55:20 +0000 (11:55 +0000)]

Improvement. Better unsigned interval propagation of BVRIGHTSHIFT.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Mar 2011 03:19:37 +0000 (03:19 +0000)]

Fix remove an extra pair of brackets from LETs. Thanks to Ayrat Khalimov.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Mar 2011 05:52:02 +0000 (05:52 +0000)]

Slight speedup to the hashing node factory.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Mar 2011 03:15:35 +0000 (03:15 +0000)]

Improvement. Create fewer objects.

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

commit | commitdiff | tree

trevor_hansen [Thu, 24 Mar 2011 01:28:52 +0000 (01:28 +0000)]

Improvement. No longer have vectors in the ASTSymbol and ASTBVConst nodes (which are always leaves). This saves 24 bytes per node.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Mar 2011 13:34:31 +0000 (13:34 +0000)]

Speedup. Short cut before some copies were created.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Mar 2011 12:04:46 +0000 (12:04 +0000)]

Move CVC parser to using strings for LET names. Removes the worst problems with names that haven't been defined being usable.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Mar 2011 05:58:12 +0000 (05:58 +0000)]

Improvement. SMTLIB2 lets now use strings for names, not SYMBOLS.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Mar 2011 05:45:36 +0000 (05:45 +0000)]

Fix the SMTLIB1 to not accept badly formed input. Previously if a variable wasn't defined it'd be implicitly defined as a boolean.

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

commit | commitdiff | tree

trevor_hansen [Wed, 23 Mar 2011 03:17:02 +0000 (03:17 +0000)]

If there are unapplied substitutions before starting unconstrained variable elimination. Then apply then.

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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