git.unchartedbackwaters.co.uk Git

khooyp [Wed, 11 Jan 2012 22:53:39 +0000 (22:53 +0000)]

Fix BitBlaster to not use the non-standard std::vector::data, for GCC-4.0 compatibility.

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

commit | commitdiff | tree

petercol [Wed, 11 Jan 2012 17:03:00 +0000 (17:03 +0000)]

Fix Clang compilation.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 16:55:46 +0000 (16:55 +0000)]

Add a C API test for the leak fixed in r1141 (when pushing/popping assertions), enabling valgrind on this test as well as another similar test.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 16:55:42 +0000 (16:55 +0000)]

Base version on local SVN change rather than the overall repository, so as not to trigger a relink and downstream rebuild.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 16:55:36 +0000 (16:55 +0000)]

Fix creation of SimplifyingNodeFactory to use STPMgr's hashingNodeFactory, to satisfy various assertions.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 16:55:28 +0000 (16:55 +0000)]

Fix BitBlaster to consistently use the hash_set macro defined in AST/UsefulDefs.h.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 16:55:23 +0000 (16:55 +0000)]

Conditionally enable -march=native, since it doesn't work in GCC on OS X.

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

commit | commitdiff | tree

khooyp [Wed, 11 Jan 2012 15:02:11 +0000 (15:02 +0000)]

Source local configuration from scripts/Makefile.local if available.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 Jan 2012 03:14:32 +0000 (03:14 +0000)]

Revert the compiler flags.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 05:53:22 +0000 (05:53 +0000)]

Improvement. Replace implementation with a node iterator.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 05:38:16 +0000 (05:38 +0000)]

* Add some extra configuration options. * Change how messages are stored.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 04:59:09 +0000 (04:59 +0000)]

Improvement. Ability to give a random number to the SAT solver.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 03:44:15 +0000 (03:44 +0000)]

Revert the makefile, I didn't mean to checkin.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 03:39:36 +0000 (03:39 +0000)]

Important bugfix. r1423 introduced a defect that gives the wrong result.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Jan 2012 03:03:23 +0000 (03:03 +0000)]

Adds an extra multiplication variant that's not enabled by default.

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

commit | commitdiff | tree

trevor_hansen [Mon, 9 Jan 2012 13:56:36 +0000 (13:56 +0000)]

Fix. Another broken assertion.

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

commit | commitdiff | tree

trevor_hansen [Mon, 9 Jan 2012 13:49:57 +0000 (13:49 +0000)]

Fix. Bad assertion, thanks to Stephan Falke.

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

commit | commitdiff | tree

trevor_hansen [Sun, 8 Jan 2012 13:00:20 +0000 (13:00 +0000)]

Add another configuration option.

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

commit | commitdiff | tree

trevor_hansen [Sun, 8 Jan 2012 12:47:44 +0000 (12:47 +0000)]

Changes to how multiplication can be encoded. No changes that effect the current operation.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 15:26:38 +0000 (15:26 +0000)]

Fix to experimental code that's not turned on.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 15:17:33 +0000 (15:17 +0000)]

Fix. Code that isn't enabled without a special config. option was broken.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 14:04:40 +0000 (14:04 +0000)]

Adds improved code and extra multiplication variants that aren't currently enabled.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 13:28:32 +0000 (13:28 +0000)]

Refactor. Remove some bad code.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 12:48:31 +0000 (12:48 +0000)]

Refactor. Automatically layout the code.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Jan 2012 12:24:39 +0000 (12:24 +0000)]

Improvement. Assert that multiplications that have no partial products true in a sum are false at the top level.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Jan 2012 13:04:33 +0000 (13:04 +0000)]

Probably a refactor. This comments out the write-refinement loop that I broke >1 year ago without realising. I'm commenting it out to prevent confusion to others. If it worked I don't know how useful it'd be.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Jan 2012 00:45:34 +0000 (00:45 +0000)]

Important Bugfix. Thanks to Khoo Yit Phang.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 Jan 2012 14:50:40 +0000 (14:50 +0000)]

Improvement. Remove an unused configuration option.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 Jan 2012 14:49:35 +0000 (14:49 +0000)]

Important Bugfix. My last checkin only initialised a variable in a constructor that isn't used.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 Jan 2012 06:26:20 +0000 (06:26 +0000)]

Fix. Remove unnecessary include that broke redhat complilation.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 Jan 2012 06:14:29 +0000 (06:14 +0000)]

Improvement. Replace difficulty and printing implementations with one that uses an iterator.

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Jan 2012 13:42:56 +0000 (13:42 +0000)]

Refactor. Replace stacks with lists.

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 Jan 2012 13:24:37 +0000 (13:24 +0000)]

Bugfix. The previous checkin broke multiplication.

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 Jan 2012 12:47:11 +0000 (12:47 +0000)]

Refactor

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 Jan 2012 02:35:12 +0000 (02:35 +0000)]

Add missing files from the last checkin.

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 Jan 2012 02:28:47 +0000 (02:28 +0000)]

Improvement. Better constant bit propagation of multiplication and division. I wanted to clean this up before checkin, but I'm short on time.

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

commit | commitdiff | tree

trevor_hansen [Mon, 2 Jan 2012 01:07:45 +0000 (01:07 +0000)]

Improvement. Extra rewriting rules.

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

commit | commitdiff | tree

trevor_hansen [Sat, 31 Dec 2011 14:51:52 +0000 (14:51 +0000)]

Improvement. Bitblasting variants can not be set from the command line.

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

commit | commitdiff | tree

trevor_hansen [Fri, 30 Dec 2011 04:09:42 +0000 (04:09 +0000)]

Refactor. Automatically layout.

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

commit | commitdiff | tree

trevor_hansen [Fri, 30 Dec 2011 04:09:15 +0000 (04:09 +0000)]

Refactor. removing namespace references in the code

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

commit | commitdiff | tree

trevor_hansen [Fri, 30 Dec 2011 03:09:30 +0000 (03:09 +0000)]

Tiny Improvement. Remove an unnecessary check.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 03:17:45 +0000 (03:17 +0000)]

Refactor. Now finised. doing what I broke in r1445/r1446.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:55:10 +0000 (02:55 +0000)]

Refactor. automatically layout code.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:50:12 +0000 (02:50 +0000)]

Improvement. Disable propagating equalities separately

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:48:43 +0000 (02:48 +0000)]

Refactor

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:15:50 +0000 (02:15 +0000)]

Refactor. Retry splitting out propagating equalities.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:04:00 +0000 (02:04 +0000)]

Refactor. Redoing the same changes in smaller pieces.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 02:00:01 +0000 (02:00 +0000)]

Bugfix. Reverting to r1445. r1446 sometimes broke.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 00:56:02 +0000 (00:56 +0000)]

Refactor. Remove propagate equalities to its own class.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Dec 2011 00:07:52 +0000 (00:07 +0000)]

Fix. If >2 arity multiplication nodes are requested. Apply associativity to give two arity multiplications.

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

commit | commitdiff | tree

trevor_hansen [Thu, 22 Dec 2011 05:30:16 +0000 (05:30 +0000)]

Refactor. rename a configuration property.

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

commit | commitdiff | tree

trevor_hansen [Thu, 22 Dec 2011 05:12:52 +0000 (05:12 +0000)]

Cleanup some of the command line parsing.

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

commit | commitdiff | tree

trevor_hansen [Thu, 22 Dec 2011 04:47:32 +0000 (04:47 +0000)]

Cleanup how the command line arguments are printed.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Dec 2011 05:14:51 +0000 (05:14 +0000)]

Improvement. If refinement is disabled, and the number of array reads is small, then re-write them all away before simplifying.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Dec 2011 02:24:01 +0000 (02:24 +0000)]

Refactor. Remove no longer used variables.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Dec 2011 02:10:40 +0000 (02:10 +0000)]

Improvement. Remove unused parameter. Better hiding.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Dec 2011 00:41:44 +0000 (00:41 +0000)]

Improvement. Better manage the data stored to revert based on difficulty.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Dec 2011 00:30:14 +0000 (00:30 +0000)]

Improvement. A better type for the polarities of the pure literal elimination.

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

commit | commitdiff | tree

trevor_hansen [Mon, 19 Dec 2011 13:53:53 +0000 (13:53 +0000)]

Improvment. When using the XOR solver, don't apply simplifications so often.

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

commit | commitdiff | tree

trevor_hansen [Wed, 30 Nov 2011 14:03:06 +0000 (14:03 +0000)]

Improvement. Generate expressions from a cleaner grammar.

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

commit | commitdiff | tree

trevor_hansen [Wed, 30 Nov 2011 13:57:18 +0000 (13:57 +0000)]

Improvement. Some missed single level size preserving rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Wed, 30 Nov 2011 11:45:55 +0000 (11:45 +0000)]

Improvements. Reduce the bit-width to speed up generation/ reduce quality.

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

commit | commitdiff | tree

trevor_hansen [Tue, 29 Nov 2011 02:24:12 +0000 (02:24 +0000)]

Utility to automatically generate rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Nov 2011 05:33:34 +0000 (05:33 +0000)]

Improvement. If simplifications make the problem containing arrays harder, then revert it. Prevsiously it only did this for bit-vector only problems. This uses extra memory. It seems justified.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Nov 2011 05:28:57 +0000 (05:28 +0000)]

Revert to r1423. I checked in the wrong file.

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

commit | commitdiff | tree

trevor_hansen [Mon, 28 Nov 2011 05:22:26 +0000 (05:22 +0000)]

commit | commitdiff | tree

trevor_hansen [Mon, 28 Nov 2011 02:55:18 +0000 (02:55 +0000)]

Improvement. Allow 128-bit indices with a compile time flag.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 Nov 2011 13:11:05 +0000 (13:11 +0000)]

Improvement. Adds half a dozen extra size preserving rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Fri, 18 Nov 2011 11:12:27 +0000 (11:12 +0000)]

Refactor. Automatically layout the code.

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

commit | commitdiff | tree

trevor_hansen [Tue, 15 Nov 2011 10:40:28 +0000 (10:40 +0000)]

Improvement. On the smtcomp2007, disabling the freaky mod/div option is now 10 percent faster than having it enabled.

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

commit | commitdiff | tree

trevor_hansen [Sun, 13 Nov 2011 12:52:09 +0000 (12:52 +0000)]

Rewrite rule changes. Left shift by a constant now rewrites to multiplication (rather than extract/concat). Adds some new rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Sun, 13 Nov 2011 12:37:29 +0000 (12:37 +0000)]

Refactor.

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

commit | commitdiff | tree

trevor_hansen [Sun, 13 Nov 2011 03:59:36 +0000 (03:59 +0000)]

Test case for r1410. Thanks to Stephan Falke.

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

commit | commitdiff | tree

raphael-michel [Thu, 10 Nov 2011 18:57:23 +0000 (18:57 +0000)]

Added my name to authors list

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

commit | commitdiff | tree

trevor_hansen [Thu, 10 Nov 2011 13:01:41 +0000 (13:01 +0000)]

Improvement. Extra c-api options from Stephan Falke.

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

commit | commitdiff | tree

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