git.unchartedbackwaters.co.uk Git

trevor_hansen [Wed, 11 May 2011 01:49:00 +0000 (01:49 +0000)]

Improvement. Add array size statistics when printing out stats.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 01:28:38 +0000 (01:28 +0000)]

Bugfix. Maybe. Disable a comparison so that CNF conversion doesn't fail. This fixes the assertion error.

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

commit | commitdiff | tree

trevor_hansen [Mon, 9 May 2011 03:57:25 +0000 (03:57 +0000)]

Adds two extra simplfication rules.

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

commit | commitdiff | tree

trevor_hansen [Mon, 9 May 2011 00:31:06 +0000 (00:31 +0000)]

More simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 May 2011 12:14:51 +0000 (12:14 +0000)]

Extra simplification rules for the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 May 2011 12:02:20 +0000 (12:02 +0000)]

Signed division now returns what is should. Signed division is defined by unsigned division. Unsigned division returns 1, if the flag is set, now signed division returns 1 or -1 as appropriate.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 May 2011 12:00:42 +0000 (12:00 +0000)]

Add a public function that calls sizeReducing until fixed point (under some conditions.)

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 May 2011 03:45:03 +0000 (03:45 +0000)]

Adds an extra BVPLUS simplification rule. Cleans up the BVPLUS rules.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 May 2011 01:46:13 +0000 (01:46 +0000)]

Important bugfix. r1291 through to this revision, about once per 200M random instances, return the wrong result.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 May 2011 00:13:34 +0000 (00:13 +0000)]

Add an extra simplification rule.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 May 2011 05:04:31 +0000 (05:04 +0000)]

Replace variables before calling the interval analysis.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 May 2011 03:53:48 +0000 (03:53 +0000)]

Function to reset the stopwatch.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 May 2011 02:45:04 +0000 (02:45 +0000)]

Another fix to the same

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 May 2011 02:41:00 +0000 (02:41 +0000)]

Correct the last patch. I don't think this code runs.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 May 2011 01:41:39 +0000 (01:41 +0000)]

Apply simplifications through arrayterms too.

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 May 2011 14:14:58 +0000 (14:14 +0000)]

Bugfix. Rarely we get the wrong answer; I got two broken instances in 140 days of fuzzing. This fixes those two instances, but, almost any change to STP fixes it, i.e. causes the problem to go away.

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

commit | commitdiff | tree

trevor_hansen [Sun, 1 May 2011 14:20:34 +0000 (14:20 +0000)]

Compiling with -D_GLIBCXX_DEBUG reported warnings because we sometimes derefferenced an iterator that was at the end. I'm not sure if this is really a problem or not..

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

commit | commitdiff | tree

trevor_hansen [Sun, 1 May 2011 12:48:53 +0000 (12:48 +0000)]

Code to apply the alwaysTrueSet. Not currently enabled.

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

commit | commitdiff | tree

trevor_hansen [Sun, 1 May 2011 03:38:53 +0000 (03:38 +0000)]

Enable bitblast simplifications by default

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 15:29:59 +0000 (15:29 +0000)]

Turn off the ite-context simplification by default.

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 12:28:07 +0000 (12:28 +0000)]

Important Bugfix. The prior checkin sometimes, but rarely, returned the wrong result.

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 05:09:02 +0000 (05:09 +0000)]

Bugfix. The last checkin caused an infinite loop (often).

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 05:00:44 +0000 (05:00 +0000)]

Extra simplification rules

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 04:18:02 +0000 (04:18 +0000)]

Extra simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Sat, 30 Apr 2011 02:07:39 +0000 (02:07 +0000)]

Convert subtraction to addition in the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Fri, 29 Apr 2011 05:57:36 +0000 (05:57 +0000)]

Bugfix. Reads might have been simplified down which was causing an assertion error.

Thanks for Yunho Kim for reporting this!

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

commit | commitdiff | tree

trevor_hansen [Wed, 27 Apr 2011 07:10:09 +0000 (07:10 +0000)]

Important Bugfix. The prior checkin causes the WRONG answer sometimes.

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

commit | commitdiff | tree

trevor_hansen [Wed, 27 Apr 2011 06:52:58 +0000 (06:52 +0000)]

Extra simplification rules. In particular a simple signed interval analysis.

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

commit | commitdiff | tree

trevor_hansen [Wed, 27 Apr 2011 02:36:30 +0000 (02:36 +0000)]

Add extra simplifying rules.

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

commit | commitdiff | tree

trevor_hansen [Wed, 27 Apr 2011 01:33:46 +0000 (01:33 +0000)]

Fix. I thought that extracts don't add any information but they do, if the underlying term has only partial fixed information.

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

commit | commitdiff | tree

trevor_hansen [Wed, 27 Apr 2011 00:37:21 +0000 (00:37 +0000)]

Remove signed division, modulus and remainder when creating nodes via the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Tue, 26 Apr 2011 23:56:29 +0000 (23:56 +0000)]

Two extra simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Thu, 21 Apr 2011 02:06:24 +0000 (02:06 +0000)]

Change the sorting network based adder (which isn't used by default).

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

commit | commitdiff | tree

trevor_hansen [Wed, 20 Apr 2011 14:23:50 +0000 (14:23 +0000)]

Refactor. Less verbose.

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

commit | commitdiff | tree

trevor_hansen [Wed, 20 Apr 2011 13:35:50 +0000 (13:35 +0000)]

Improvement. Add a warning when parsing problems that use array extensionality.

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

commit | commitdiff | tree

trevor_hansen [Sat, 16 Apr 2011 13:32:28 +0000 (13:32 +0000)]

Extra upfront simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Thu, 14 Apr 2011 06:34:08 +0000 (06:34 +0000)]

Add some missing simplification rules for AND/OR/ propositional ITE.

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

commit | commitdiff | tree

trevor_hansen [Thu, 14 Apr 2011 05:32:21 +0000 (05:32 +0000)]

Shortcut in a rare circumstance.

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

commit | commitdiff | tree

trevor_hansen [Thu, 14 Apr 2011 05:31:06 +0000 (05:31 +0000)]

Extra BVXOR simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 14:21:58 +0000 (14:21 +0000)]

Adds the reverse of rules to catch an obscure but important for some of our benchmarks rule.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 12:58:34 +0000 (12:58 +0000)]

Improvement. Add a warning message when using --exit-after-CNF with arrays, without -r.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 12:41:03 +0000 (12:41 +0000)]

Improvement. Fix the difficulty score for subtraction.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 04:52:49 +0000 (04:52 +0000)]

Fix the build. Without -NDEBUG wouldn't compile.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 04:41:09 +0000 (04:41 +0000)]

Improvement. Look for nodes that are true/false when conjoined to the top.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 04:30:17 +0000 (04:30 +0000)]

Remove some assertions that don't necessarily hold.

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

commit | commitdiff | tree

trevor_hansen [Wed, 13 Apr 2011 02:00:29 +0000 (02:00 +0000)]

Improvement. Replace the hashing node factory with the simplifying node factory. Add an extra obscure simplification rule.

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

commit | commitdiff | tree

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