git.unchartedbackwaters.co.uk Git

trevor_hansen [Mon, 6 Feb 2012 12:23:15 +0000 (12:23 +0000)]

Add code to do maximally precise transformer via Reps.

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

commit | commitdiff | tree

trevor_hansen [Mon, 6 Feb 2012 12:07:49 +0000 (12:07 +0000)]

Fix. Get it the utility compiling.

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

commit | commitdiff | tree

trevor_hansen [Mon, 6 Feb 2012 12:04:18 +0000 (12:04 +0000)]

Include a utliity to measure the cbitp time.

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

commit | commitdiff | tree

trevor_hansen [Sat, 4 Feb 2012 04:07:49 +0000 (04:07 +0000)]

Remove debugging message.

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

commit | commitdiff | tree

trevor_hansen [Sat, 4 Feb 2012 03:27:27 +0000 (03:27 +0000)]

Enable bit-blaster equivalency checking by default.

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

commit | commitdiff | tree

trevor_hansen [Fri, 3 Feb 2012 14:28:35 +0000 (14:28 +0000)]

Improvement. Cleanup how the bb equivalent vector operations are enabled.

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

commit | commitdiff | tree

trevor_hansen [Fri, 3 Feb 2012 14:12:30 +0000 (14:12 +0000)]

Improvement. Use AIGs to find semantically equivalent but syntactically distinct ASTNodes.

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

commit | commitdiff | tree

trevor_hansen [Fri, 3 Feb 2012 12:59:16 +0000 (12:59 +0000)]

disable sbvmod propagator.

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

commit | commitdiff | tree

trevor_hansen [Fri, 3 Feb 2012 03:41:30 +0000 (03:41 +0000)]

Improvement. Use the results of bit-blasting to detect equivalent predicates. Currently disabled by default until I finish testing.

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

commit | commitdiff | tree

trevor_hansen [Thu, 2 Feb 2012 12:29:35 +0000 (12:29 +0000)]

Search for a AND (NOT a), a OR (NOT a), when doing node creation. This is necessary on some sage benchmarks.

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

commit | commitdiff | tree

trevor_hansen [Thu, 2 Feb 2012 12:28:24 +0000 (12:28 +0000)]

A fixed version r1547. I missed a bound.

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

commit | commitdiff | tree

trevor_hansen [Thu, 2 Feb 2012 12:09:25 +0000 (12:09 +0000)]

Revert. The prior change to min/max has some problem I don't understand yet.

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

commit | commitdiff | tree

trevor_hansen [Thu, 2 Feb 2012 11:40:05 +0000 (11:40 +0000)]

Improvement. 10x better min and max value out of the sets of fixed bits.

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

commit | commitdiff | tree

trevor_hansen [Wed, 1 Feb 2012 12:36:24 +0000 (12:36 +0000)]

Small speedup. Remove redundant initialisation.

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

commit | commitdiff | tree

trevor_hansen [Tue, 31 Jan 2012 14:17:02 +0000 (14:17 +0000)]

Refactor. Automatically layout.

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

commit | commitdiff | tree

trevor_hansen [Tue, 31 Jan 2012 14:14:22 +0000 (14:14 +0000)]

Improvement. This makes the multiplication propagator less dumb.

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

commit | commitdiff | tree

trevor_hansen [Tue, 31 Jan 2012 10:32:46 +0000 (10:32 +0000)]

Improvement. Better leading zero detection in the multiplication propagator.

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

commit | commitdiff | tree

trevor_hansen [Tue, 31 Jan 2012 03:19:13 +0000 (03:19 +0000)]

Improvement, if there are < 10 array reads, write them away upfront.

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

commit | commitdiff | tree

trevor_hansen [Tue, 31 Jan 2012 01:12:24 +0000 (01:12 +0000)]

Adds extra code that is not enabled by default.

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

commit | commitdiff | tree

trevor_hansen [Mon, 30 Jan 2012 03:28:39 +0000 (03:28 +0000)]

Improvement. For some bechmarks anyway. Completely bit-blast small problems when deciding on whether to revert them based on difficulty.

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

commit | commitdiff | tree

trevor_hansen [Sun, 29 Jan 2012 12:20:22 +0000 (12:20 +0000)]

Remove implication graph code. It's too slow to be useful.

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

commit | commitdiff | tree

trevor_hansen [Sun, 29 Jan 2012 02:48:15 +0000 (02:48 +0000)]

Improvement. Generalise fixing of trailing zeroes in multiplication.

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

commit | commitdiff | tree

trevor_hansen [Sun, 29 Jan 2012 02:12:31 +0000 (02:12 +0000)]

Improvement. Generalise the equality check when exaustively generating equations.

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

commit | commitdiff | tree

trevor_hansen [Sat, 28 Jan 2012 13:57:37 +0000 (13:57 +0000)]

Fix an assertion error.

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

commit | commitdiff | tree

trevor_hansen [Sat, 28 Jan 2012 04:08:17 +0000 (04:08 +0000)]

Make another class noncopyable.

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

commit | commitdiff | tree

trevor_hansen [Sat, 28 Jan 2012 04:02:57 +0000 (04:02 +0000)]

Improvement. Enable the simplifying node factory by default for the SMT, SMT2 and CVC3 languages.

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

commit | commitdiff | tree

trevor_hansen [Sat, 28 Jan 2012 03:54:46 +0000 (03:54 +0000)]

Add the cloud9 test cases to regressall.

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

commit | commitdiff | tree

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