git.unchartedbackwaters.co.uk Git

trevor_hansen [Thu, 10 Nov 2011 12:45:04 +0000 (12:45 +0000)]

Remove old command line flags.

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

commit | commitdiff | tree

trevor_hansen [Thu, 10 Nov 2011 11:57:35 +0000 (11:57 +0000)]

Improvement. Add the ability to set SAT solvers via the command line. Thanks to Stephan Falke.

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

commit | commitdiff | tree

trevor_hansen [Sat, 22 Oct 2011 12:12:28 +0000 (12:12 +0000)]

Improvement. The default array solver is now built into the SAT solver so SAT solving doesn't need to start/stop to do refinement.

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

commit | commitdiff | tree

trevor_hansen [Mon, 17 Oct 2011 11:45:45 +0000 (11:45 +0000)]

Cleanup a bit. Include suggestion from Oliver Crameri.

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

commit | commitdiff | tree

trevor_hansen [Mon, 17 Oct 2011 11:34:16 +0000 (11:34 +0000)]

Fix. Print back CVC wasn't prininting back all of the input.

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

commit | commitdiff | tree

trevor_hansen [Sat, 15 Oct 2011 13:45:09 +0000 (13:45 +0000)]

Fix the prior checkin. I left a debug message turned on.

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

commit | commitdiff | tree

trevor_hansen [Sat, 15 Oct 2011 13:43:22 +0000 (13:43 +0000)]

Experimental change. Do an expensive check if the index of the read equals the index of the write.

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

commit | commitdiff | tree

trevor_hansen [Wed, 12 Oct 2011 00:01:07 +0000 (00:01 +0000)]

Fix mismatched malloc/delete as reported by Edward Schwartz.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Sep 2011 12:59:42 +0000 (12:59 +0000)]

Add a disable all simplifications option.

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Sep 2011 13:35:36 +0000 (13:35 +0000)]

Ooops. Add the fix.

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Sep 2011 13:35:03 +0000 (13:35 +0000)]

Bugfix. Couldn't create booleans via the interface. Thanks to Stephan Falke.

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

commit | commitdiff | tree

trevor_hansen [Tue, 13 Sep 2011 10:37:34 +0000 (10:37 +0000)]

Improvment. Don't run destructors by default, just exit.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Sep 2011 14:58:35 +0000 (14:58 +0000)]

Improvement. speed up checking for array terms.

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

commit | commitdiff | tree

trevor_hansen [Sun, 11 Sep 2011 13:41:14 +0000 (13:41 +0000)]

Improvement. run unconstrained elimination after propagating equalities. Unconstrained is the more expensive, so running the other one first can shrink the size of the problem down before it runs.

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

commit | commitdiff | tree

trevor_hansen [Sun, 11 Sep 2011 12:53:41 +0000 (12:53 +0000)]

Improvement. Speedup checking for changes by just comparing the number of fixed bits.

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

commit | commitdiff | tree

trevor_hansen [Sun, 11 Sep 2011 12:44:55 +0000 (12:44 +0000)]

This fuzzer now outputs lots of files to the current directory.

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

commit | commitdiff | tree

trevor_hansen [Thu, 1 Sep 2011 12:29:37 +0000 (12:29 +0000)]

Bugfix. Thanks for Jianjun Huang for the report. If the simplifying node factory wasn't enabled, the types were sometimes wrong.

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

commit | commitdiff | tree

trevor_hansen [Wed, 31 Aug 2011 04:02:27 +0000 (04:02 +0000)]

extra debug message.

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

commit | commitdiff | tree

trevor_hansen [Mon, 22 Aug 2011 15:15:00 +0000 (15:15 +0000)]

Improvement. Wrap most of the calls to bvtypecheck in assert(), so that disabling assertions will remove them. Cleanup woeful duplication.

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

commit | commitdiff | tree

trevor_hansen [Sat, 13 Aug 2011 21:48:23 +0000 (21:48 +0000)]

Bugfix. Some array reads were not removed as is required. This caused an assertion error.

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

commit | commitdiff | tree

trevor_hansen [Thu, 11 Aug 2011 12:54:25 +0000 (12:54 +0000)]

Add ability to use CMS2 via the c-interface.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 15:08:07 +0000 (15:08 +0000)]

Trialing adding a symbolic link. Cristian Cadar wants a copy of c_interface.h to be here somehow. A symbolic link seems one way to do it...

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 14:06:23 +0000 (14:06 +0000)]

Improvement. Only set the install prefix if the enviroment variable is not set.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 07:07:44 +0000 (07:07 +0000)]

Extra capi checks.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 05:25:34 +0000 (05:25 +0000)]

Fix. If the c-interface was used to create nodes, then there would be an infinite loop on the input ite(4=6,4,2).

Thanks to Jingyue Wu for providing this patch.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 05:15:54 +0000 (05:15 +0000)]

Interface Change. The c-interface now uses the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Aug 2011 04:17:09 +0000 (04:17 +0000)]

Bugfix. #x notation for hex literals did not work.

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

commit | commitdiff | tree

trevor_hansen [Sat, 6 Aug 2011 04:02:44 +0000 (04:02 +0000)]

Add unconstrained shift for left/right.

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

commit | commitdiff | tree

trevor_hansen [Fri, 29 Jul 2011 15:33:16 +0000 (15:33 +0000)]

extra unit test

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

commit | commitdiff | tree

trevor_hansen [Tue, 26 Jul 2011 05:22:26 +0000 (05:22 +0000)]

Bugfix. If nodes are created with just the hashing node factory (not with the simplifying node factory). Then sometimes an infinite loop happened.

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

commit | commitdiff | tree

trevor_hansen [Mon, 18 Jul 2011 05:23:24 +0000 (05:23 +0000)]

Improvement. Sort partial products in the multiplication.

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 12:31:42 +0000 (12:31 +0000)]

Improvement. Maybe. Left recursion is supposed to be better. i.e. to use less stack space. When I measured it just now it used the same amount....

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 12:25:32 +0000 (12:25 +0000)]

Output the peak memory used when using -s.

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 11:58:32 +0000 (11:58 +0000)]

Fix to get it compiling with Cygwin. Thanks to Marzio De Biasi.

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 07:04:35 +0000 (07:04 +0000)]

Fix. unit_test script was not working. Adds another test.

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 06:17:00 +0000 (06:17 +0000)]

Bugfix. Thanks to Jingyue Wu for reporting sbvdiv was broken through the c-api.

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 05:09:42 +0000 (05:09 +0000)]

Patch from Peter Collingbourne to enable compiling with clang. Thanks\!

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

commit | commitdiff | tree

trevor_hansen [Tue, 12 Jul 2011 05:06:59 +0000 (05:06 +0000)]

Remove the include directory. It shouldn't be here.

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

commit | commitdiff | tree

trevor_hansen [Sat, 9 Jul 2011 06:56:51 +0000 (06:56 +0000)]

Fix. The SMTLIB2 parser now outputs "success" in reply to commands if the option is enabled.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 10:48:46 +0000 (10:48 +0000)]

Move functions around so that clang links.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:57:48 +0000 (06:57 +0000)]

Remove clang warnings.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:45:58 +0000 (06:45 +0000)]

Fix clang warnings.

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

commit | commitdiff | tree

trevor_hansen [Thu, 7 Jul 2011 06:34:54 +0000 (06:34 +0000)]

Silence a clang warning message.

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

commit | commitdiff | tree

trevor_hansen [Thu, 30 Jun 2011 15:33:11 +0000 (15:33 +0000)]

Improvement. Needed for using STP interactively.

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

commit | commitdiff | tree

trevor_hansen [Mon, 27 Jun 2011 02:12:57 +0000 (02:12 +0000)]

Adds the push(n) and pop(n) instructions to the SMTLIB2 command language. Previously hitting the EOF would trigger a check for satisfiability. Now, you need to explicitly call (check-sat).

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

commit | commitdiff | tree

trevor_hansen [Sun, 26 Jun 2011 16:23:55 +0000 (16:23 +0000)]

Move the filename counter out so it's saved between CNF converter objects.

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

commit | commitdiff | tree

trevor_hansen [Sun, 26 Jun 2011 15:14:31 +0000 (15:14 +0000)]

Improvement. Additional simplification rules.

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

commit | commitdiff | tree

trevor_hansen [Thu, 23 Jun 2011 06:06:59 +0000 (06:06 +0000)]

Fix. Look for fatal errors when running tests.

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

commit | commitdiff | tree

trevor_hansen [Thu, 23 Jun 2011 02:17:24 +0000 (02:17 +0000)]

Improvement. Simplifying minisat now uses the advanced CNF generator by default.

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

commit | commitdiff | tree

trevor_hansen [Wed, 22 Jun 2011 06:28:23 +0000 (06:28 +0000)]

Improvement. Create fewer clauses when creating an array axiom. I was adding extra variables that weren't required.

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

commit | commitdiff | tree

trevor_hansen [Tue, 21 Jun 2011 14:06:48 +0000 (14:06 +0000)]

Automatically format this code. No semantic change.

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

commit | commitdiff | tree

trevor_hansen [Tue, 21 Jun 2011 14:04:48 +0000 (14:04 +0000)]

Check axioms for indexes in order of the number of constants that they have. Adds some extra code for applying all the axioms that is currently disabled..

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

commit | commitdiff | tree

trevor_hansen [Mon, 20 Jun 2011 14:15:13 +0000 (14:15 +0000)]

Improvement. During abstraction refinement process arrays in order of the number of indexes.

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

commit | commitdiff | tree

trevor_hansen [Mon, 20 Jun 2011 05:26:31 +0000 (05:26 +0000)]

Fix. I forgot to remove the descriptions of -e -f from help.

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

commit | commitdiff | tree

trevor_hansen [Mon, 20 Jun 2011 05:17:02 +0000 (05:17 +0000)]

Remove the code for the not-working FOR construct.

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

commit | commitdiff | tree

trevor_hansen [Mon, 20 Jun 2011 04:29:10 +0000 (04:29 +0000)]

Vijay advised we aren't going to do fors.

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

commit | commitdiff | tree

trevor_hansen [Sun, 19 Jun 2011 09:06:06 +0000 (09:06 +0000)]

Use the advanced CNF generator to encode array problems into CNF. Array axioms are generated by hand. NB. This slows down the CVC regressions substantially. Adding about 40 seconds to them. The CVC array problems are very easy, so the extra effort in generating a better CNF is wasted.

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

commit | commitdiff | tree

trevor_hansen [Thu, 16 Jun 2011 05:31:00 +0000 (05:31 +0000)]

Add boost to the licence, fix bitvector description.

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

commit | commitdiff | tree

trevor_hansen [Thu, 16 Jun 2011 03:54:40 +0000 (03:54 +0000)]

Bugfix. Fix the semantics of BVSMOD to always give the remainder rounding towards zero.

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

commit | commitdiff | tree

trevor_hansen [Thu, 16 Jun 2011 02:19:27 +0000 (02:19 +0000)]

Speedup for easy instances. Don't call the SAT solver if we already know the problem is true/false.

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

commit | commitdiff | tree

trevor_hansen [Tue, 14 Jun 2011 12:53:10 +0000 (12:53 +0000)]

Add cloud9 test cases.

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Jun 2011 04:28:54 +0000 (04:28 +0000)]

A windows patch to r446 from Hume.

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

commit | commitdiff | tree

trevor_hansen [Thu, 12 May 2011 04:56:59 +0000 (04:56 +0000)]

Improvement. Make error checking more normal.

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

commit | commitdiff | tree

trevor_hansen [Thu, 12 May 2011 04:28:04 +0000 (04:28 +0000)]

Extra simplification rule.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 05:17:11 +0000 (05:17 +0000)]

Extra test cases that simplify down to nothing.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 05:14:36 +0000 (05:14 +0000)]

ITE context is mostly bad. Now disabled by default.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 04:24:39 +0000 (04:24 +0000)]

No longer default to the simple CNF generator for big AIGs, i.e >=2Million nodes. We used to do this because of a bug(?) now fixed in ABC.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 04:23:04 +0000 (04:23 +0000)]

Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We used to read the CNF back out of the SAT solver, but don't any longer, so there's no reason to do this.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 04:15:15 +0000 (04:15 +0000)]

Fix. Creating the node (v + v), where v is greater than 64 bits would fail.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 03:34:42 +0000 (03:34 +0000)]

Bugfix. Arithmetic shifts by constants that didn't fit in 32-bits would cause an assertion error.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 01:57:12 +0000 (01:57 +0000)]

Revert the change to run_tests, I didn't mean to submit this.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 May 2011 01:53:42 +0000 (01:53 +0000)]

Remove the comment that 32-bit is best for arrays. No longer the case because we use ABC's AIG CNF conversion by default.

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

commit | commitdiff | tree

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