git.unchartedbackwaters.co.uk Git

trevor_hansen [Sat, 28 Jan 2012 02:18:09 +0000 (02:18 +0000)]

Improvement. We missed an unusual case when deciding whether to substitute variables.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 13:14:41 +0000 (13:14 +0000)]

Improvement. Patch ABC to replace the standard popcount with a partialy unrolled wegner popcount. About ten percent faster.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 11:36:55 +0000 (11:36 +0000)]

Fix to the prior checkin. It was completely wrong.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 09:09:34 +0000 (09:09 +0000)]

Improvement. Don't clean up the advanced CNF generator after it's been called >1 time. This makes solving a stream of 2000 easy problems twice as fast.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 05:56:54 +0000 (05:56 +0000)]

Fix the SMTLIB2 application language parser.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 05:04:55 +0000 (05:04 +0000)]

Improvement. The SMT-LIB2 parser no longer stores a copy of the asserts/query locally. It uses the stored one.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 04:23:02 +0000 (04:23 +0000)]

Cleanup. This removes some of the code for the user controlled abstraction-refinement. I don't know if this code worked or not. There aren't any test cases that use it, so it might be broken. Removing this makes some changes I'm trying to make much easier. Sorry if you use it. Let me know. Trev.

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

commit | commitdiff | tree

trevor_hansen [Thu, 26 Jan 2012 03:35:05 +0000 (03:35 +0000)]

Fix the rewrite generator to compile.

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 12:54:59 +0000 (12:54 +0000)]

Improvement. Do better trailing zero propagation on multiplication.

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 04:32:40 +0000 (04:32 +0000)]

Fix comment.:

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 04:26:37 +0000 (04:26 +0000)]

Improvement. Add the ability to set a soft timeout via the c_interface. You specify the number of milliseconds that you want STP to run for.

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 01:25:17 +0000 (01:25 +0000)]

Clean up. I think this is just a refactor, but aren't sure. The c_interface set removewrites to true sometimes. It was the only place in the code that set it...

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 00:49:15 +0000 (00:49 +0000)]

Refactor. Automatically layout code.

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 00:48:40 +0000 (00:48 +0000)]

Refactor. Rename parserinterface to cpp_interface.

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

commit | commitdiff | tree

trevor_hansen [Tue, 24 Jan 2012 00:38:46 +0000 (00:38 +0000)]

Refactor. First step in moving the parser interface to be the cpp interface.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Jan 2012 22:51:23 +0000 (22:51 +0000)]

Fix the build again.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Jan 2012 22:45:54 +0000 (22:45 +0000)]

Fix the build. Spotted by Vijay Ganesh, Spencer Whitman and Stephan Falke. Ta.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Jan 2012 12:43:59 +0000 (12:43 +0000)]

Fix. Thanks to Stephan Falke. Last checkin put a dependency on boost being installed on the machine.

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

commit | commitdiff | tree

trevor_hansen [Sun, 22 Jan 2012 12:34:38 +0000 (12:34 +0000)]

Mark most of the classes that shouldn't be copied as noncopyable.

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

commit | commitdiff | tree

trevor_hansen [Sat, 21 Jan 2012 00:24:03 +0000 (00:24 +0000)]

Improvement. Remove the do-not-solve-for set. I suspect this is no longer needed. The substitution map checks thoroughly whether substitutions can be made, so I think the old set is redundant.

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

commit | commitdiff | tree

trevor_hansen [Fri, 20 Jan 2012 23:55:14 +0000 (23:55 +0000)]

Remove the xor solver from the bvsolver. XORs are now captured in propagateEqualities.

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

commit | commitdiff | tree

trevor_hansen [Tue, 17 Jan 2012 03:00:59 +0000 (03:00 +0000)]

Improvement. Rewrite the Equality Propagation code to be conceptially pure.

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

commit | commitdiff | tree

trevor_hansen [Mon, 16 Jan 2012 02:17:13 +0000 (02:17 +0000)]

Refactor. Add an extra configuration option to control always_true detection.

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

commit | commitdiff | tree

trevor_hansen [Mon, 16 Jan 2012 01:41:14 +0000 (01:41 +0000)]

Refactor.

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

commit | commitdiff | tree

trevor_hansen [Sat, 14 Jan 2012 03:02:38 +0000 (03:02 +0000)]

Extra unit tests.

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

commit | commitdiff | tree

trevor_hansen [Sat, 14 Jan 2012 02:16:46 +0000 (02:16 +0000)]

Extra unit test.

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

commit | commitdiff | tree

trevor_hansen [Thu, 12 Jan 2012 00:35:28 +0000 (00:35 +0000)]

Remove a clang warning. No change.

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

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

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

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

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

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

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

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

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