git.unchartedbackwaters.co.uk Git

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

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