git.unchartedbackwaters.co.uk Git

trevor_hansen [Mon, 9 Apr 2012 13:21:26 +0000 (13:21 +0000)]

Improvement. In general it seems that these optsions are better than the prior ones.

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

commit | commitdiff | tree

trevor_hansen [Sun, 8 Apr 2012 06:30:34 +0000 (06:30 +0000)]

Improvements to utility code for timing cbitp propagators.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Apr 2012 12:43:20 +0000 (12:43 +0000)]

Refactor. Automatically format the code, no other change.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Apr 2012 12:42:23 +0000 (12:42 +0000)]

Small improvements to the multiplication propagator.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Apr 2012 00:43:51 +0000 (00:43 +0000)]

Improvement. Fix an oddity which required a method to be called right after construction.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Apr 2012 00:21:57 +0000 (00:21 +0000)]

Adds a utility to parse smt-lib2, constant bit propagate, then output the result.

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

commit | commitdiff | tree

trevor_hansen [Sat, 7 Apr 2012 00:20:57 +0000 (00:20 +0000)]

Improvement. Change how the bitblast equivalence checking is enabled.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Apr 2012 03:55:50 +0000 (03:55 +0000)]

Improvement. Add a configuration option to remove a simplification, reduce its limit too.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Apr 2012 01:20:11 +0000 (01:20 +0000)]

Improvement. Output configuration flags in the same format they are set.

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

commit | commitdiff | tree

trevor_hansen [Thu, 5 Apr 2012 01:13:21 +0000 (01:13 +0000)]

Fix to the SMTLIB2 printer. Symbols with spaces in the name didn't get output properly.

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

commit | commitdiff | tree

trevor_hansen [Wed, 4 Apr 2012 02:43:37 +0000 (02:43 +0000)]

improvement. Add the ability to the cpp interface to ignore calls to sat.

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Apr 2012 15:08:25 +0000 (15:08 +0000)]

Improvement to cbipt. Run unsigned division propagagtor instead of the signed division propagator if both values are positive.

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Apr 2012 12:32:10 +0000 (12:32 +0000)]

Fix the build. With assertions enabled it would not compile.

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Apr 2012 12:30:52 +0000 (12:30 +0000)]

Fix some more test cases by returning from main.

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Apr 2012 09:45:54 +0000 (09:45 +0000)]

Fix. Put in a return value from main

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

commit | commitdiff | tree

trevor_hansen [Tue, 3 Apr 2012 06:43:00 +0000 (06:43 +0000)]

Improvements. Move the hard timeout function to a utility file, apply max. precise propagators in cbitp.

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

commit | commitdiff | tree

trevor_hansen [Thu, 29 Mar 2012 23:33:56 +0000 (23:33 +0000)]

Improvements to measurement code.

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Mar 2012 12:10:37 +0000 (12:10 +0000)]

Improvements to utility code.

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

commit | commitdiff | tree

trevor_hansen [Tue, 27 Mar 2012 11:44:05 +0000 (11:44 +0000)]

Improvement. Better propagate bits when there is a division by zero possible.

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

commit | commitdiff | tree

trevor_hansen [Mon, 26 Mar 2012 11:45:42 +0000 (11:45 +0000)]

Big speedup to utility code for producing the effect of the maximally precise propagator.

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

commit | commitdiff | tree

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