]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
trevor_hansen [Mon, 28 Nov 2011 05:22:26 +0000 (05:22 +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@1425
e59a4935 -1847-0410-ae03-
e826735625c1
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
projects / francis / stp.git / log