git.unchartedbackwaters.co.uk Git

trevor_hansen [Sun, 25 Mar 2012 23:20:58 +0000 (23:20 +0000)]

Improvements to utility code. Less outputting to cerr, different semantics for expand.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 05:33:03 +0000 (05:33 +0000)]

Important Bugfix. The recently introduced bvmod simplifications are wrong.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 05:04:01 +0000 (05:04 +0000)]

Improvement. Better propagation for division when division be zero is possible.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 05:00:47 +0000 (05:00 +0000)]

Improvement. Two extra simplifications for the bvmod

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 04:43:41 +0000 (04:43 +0000)]

Improvements to the utility code for generating rewrites.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 04:40:50 +0000 (04:40 +0000)]

Utility code. When deleting duplicate rewrite rules, keep the instance that's verified to the highest bit-width.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 01:37:12 +0000 (01:37 +0000)]

Fix to the last checkin, remove a debugging output.

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

commit | commitdiff | tree

trevor_hansen [Sun, 25 Mar 2012 01:35:28 +0000 (01:35 +0000)]

Improvement. If the numerator of a division contains leading zeroes, replace the division with a concatenation. Thanks to Edward Schwartz for providing the test case to inspire this.

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

commit | commitdiff | tree

trevor_hansen [Tue, 20 Mar 2012 03:59:03 +0000 (03:59 +0000)]

Improvement. Use the default node factory rather than specifying a node factory in some places like I used to do.

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

commit | commitdiff | tree

trevor_hansen [Mon, 19 Mar 2012 00:31:21 +0000 (00:31 +0000)]

Improvements to utility code for generating rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Sun, 18 Mar 2012 05:53:52 +0000 (05:53 +0000)]

Improvement to the utility code for building rewrites.

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

commit | commitdiff | tree

trevor_hansen [Sat, 17 Mar 2012 12:07:57 +0000 (12:07 +0000)]

Fix. Some of the test cases are now build with the c-compiler rather than just the C++ compiler. Thanks to Spencer Whitman for informing us.

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

commit | commitdiff | tree

trevor_hansen [Sat, 17 Mar 2012 11:51:42 +0000 (11:51 +0000)]

Changes to the C-interface. I forgot that C doesn't allow default arguments, this rectifies the mistake, but will break any recently written code that uses the timeout functionality.

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

commit | commitdiff | tree

trevor_hansen [Thu, 15 Mar 2012 12:38:21 +0000 (12:38 +0000)]

Beautification. Pointer to the base class instead of the derived class.

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

commit | commitdiff | tree

trevor_hansen [Thu, 15 Mar 2012 12:37:25 +0000 (12:37 +0000)]

Fix. Don't use the global nodefactory when we have a local one.

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

commit | commitdiff | tree

trevor_hansen [Thu, 15 Mar 2012 12:36:26 +0000 (12:36 +0000)]

Fixes to code for manipulating rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Mar 2012 14:12:39 +0000 (14:12 +0000)]

Refactor utility code. Automatically layout, no other changes.

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Mar 2012 14:11:17 +0000 (14:11 +0000)]

Miscellaneous fixes to rewrite generation.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 11:34:20 +0000 (11:34 +0000)]

Improvements to rewrite utility code.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:11:58 +0000 (04:11 +0000)]

Check not and minus better when type checking.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:07:37 +0000 (04:07 +0000)]

Remove an unimplemented function from a header.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:06:44 +0000 (04:06 +0000)]

Add the ability to tell the SMTLIB2 printer whether it contains arrays or not. The array check can be very expensive.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:04:57 +0000 (04:04 +0000)]

Improvements. Better preventing infinite loops when rewriting replacements through.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:03:24 +0000 (04:03 +0000)]

Remove unused code.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 04:01:56 +0000 (04:01 +0000)]

Improvements to the code for generating rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 01:04:49 +0000 (01:04 +0000)]

Move the time function to global scope.

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

commit | commitdiff | tree

trevor_hansen [Mon, 12 Mar 2012 00:12:51 +0000 (00:12 +0000)]

Adds the simplify and nclauses methods to some SAT solvers.

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

commit | commitdiff | tree

trevor_hansen [Tue, 6 Mar 2012 00:08:29 +0000 (00:08 +0000)]

Improvements to rewrite utility code.

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Mar 2012 23:26:16 +0000 (23:26 +0000)]

Improvements to utility code.

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

commit | commitdiff | tree

trevor_hansen [Sun, 4 Mar 2012 23:03:33 +0000 (23:03 +0000)]

This removes some rewrite rules that I haven't yet tested enough.:

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 12:16:56 +0000 (12:16 +0000)]

Improvement. Extra rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 12:15:42 +0000 (12:15 +0000)]

Improvements to the utility for generating rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 11:59:10 +0000 (11:59 +0000)]

New cpp interface function to pop away asserts.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 01:56:43 +0000 (01:56 +0000)]

Improvement to utility code. Replace directly accessing arrays with iterators.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 00:51:56 +0000 (00:51 +0000)]

Remove an unnecessary file.

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

commit | commitdiff | tree

trevor_hansen [Sat, 3 Mar 2012 00:50:53 +0000 (00:50 +0000)]

Extra utility code for manipulating rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Wed, 29 Feb 2012 03:56:16 +0000 (03:56 +0000)]

Fix. I used the wrong comparison operation.

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

commit | commitdiff | tree

trevor_hansen [Mon, 27 Feb 2012 12:56:07 +0000 (12:56 +0000)]

Improvement. Sometimes the interface throws division by zero errors, making division a total function avoids them. Thanks to Tom Bergan for reporting the problem.

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

commit | commitdiff | tree

trevor_hansen [Wed, 22 Feb 2012 12:54:53 +0000 (12:54 +0000)]

Cleanup the utility code for off-line generation of candidate rewrite rules.

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

commit | commitdiff | tree

trevor_hansen [Mon, 20 Feb 2012 03:54:20 +0000 (03:54 +0000)]

Improvement. The bitblaster now handled signed div/mod/rem. They don't need to be removed before bitblasting.

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

commit | commitdiff | tree

trevor_hansen [Sat, 18 Feb 2012 12:37:48 +0000 (12:37 +0000)]

Refactor - automatically layout code, and move one big function out of the header file.

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

commit | commitdiff | tree

trevor_hansen [Sat, 18 Feb 2012 12:33:43 +0000 (12:33 +0000)]

Improvement. Write the equivalences that the bit-blaster discovers through transitively.

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

commit | commitdiff | tree

trevor_hansen [Fri, 17 Feb 2012 13:48:39 +0000 (13:48 +0000)]

Improvements speedups for better test code.

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Feb 2012 03:46:58 +0000 (03:46 +0000)]

Turn on bit-blast equivalency detection again.

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Feb 2012 02:42:21 +0000 (02:42 +0000)]

Important bugfix. This rewrite rule implemented the wrong semantics for /0. It used to be 0/x -> 0, rather than 0/x -> ite(x=0,1,0).

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Feb 2012 00:35:43 +0000 (00:35 +0000)]

Disable bit-blast equivalence checking, it returns the wrong answer sometimes.

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Feb 2012 00:16:20 +0000 (00:16 +0000)]

Fix the build. Typo in last checkin.

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

commit | commitdiff | tree

trevor_hansen [Thu, 9 Feb 2012 00:13:20 +0000 (00:13 +0000)]

Fix. The new bit-blast simplifications where only half working.

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

commit | commitdiff | tree

trevor_hansen [Wed, 8 Feb 2012 12:57:03 +0000 (12:57 +0000)]

Turn off more things when disabling simplify.

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

commit | commitdiff | tree

trevor_hansen [Tue, 7 Feb 2012 14:32:09 +0000 (14:32 +0000)]

Disable signed bvmod propagator, I think it implements old style semantics. Add a test function to compare propagators against the effect of the maximally precise propagator.

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

commit | commitdiff | tree

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