git.unchartedbackwaters.co.uk Git

trevor_hansen [Sun, 24 Feb 2013 03:35:00 +0000 (03:35 +0000)]

Fix the build for propagator utilities.

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

commit | commitdiff | tree

trevor_hansen [Sun, 24 Feb 2013 03:29:47 +0000 (03:29 +0000)]

Fix the utilities for measuring the precision of propagators.

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Feb 2013 12:49:20 +0000 (12:49 +0000)]

Print out SBVMOD Nodes. Thanks to Jingyue Wu.

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Feb 2013 12:39:06 +0000 (12:39 +0000)]

Patch from Trevor Woerner to compile on OpenSuSE 12.2. thanks

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

commit | commitdiff | tree

trevor_hansen [Mon, 11 Feb 2013 12:31:52 +0000 (12:31 +0000)]

Fix c-api parsing of CVC strings. Thanks to Ryan Govostes for reporting.

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

commit | commitdiff | tree

trevor_hansen [Wed, 3 Oct 2012 00:08:34 +0000 (00:08 +0000)]

Speedup for AND/OR with lots of sharing to fix the testcase of 1667. Thanks to Carsten Sinz.

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

commit | commitdiff | tree

trevor_hansen [Fri, 15 Jun 2012 14:40:15 +0000 (14:40 +0000)]

Fix the build. Remove code I didn't mean to checkin.

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

commit | commitdiff | tree

trevor_hansen [Fri, 15 Jun 2012 14:28:01 +0000 (14:28 +0000)]

Partial implementation of the SMT-LIB2 define function syntax. Won't work with push/pop.

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

commit | commitdiff | tree

trevor_hansen [Sat, 26 May 2012 06:24:52 +0000 (06:24 +0000)]

small improvement. Pull up bvnot from bvarshift.

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

commit | commitdiff | tree

trevor_hansen [Fri, 25 May 2012 13:36:17 +0000 (13:36 +0000)]

Remove unnecessary code when cancelling. Thanks to Graeme Gange for pointing this out.

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

commit | commitdiff | tree

trevor_hansen [Sat, 12 May 2012 02:18:08 +0000 (02:18 +0000)]

Change -r so that it produces simpler expressions. I changed it in a way I didn't expect long ago.

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

commit | commitdiff | tree

trevor_hansen [Mon, 30 Apr 2012 14:32:57 +0000 (14:32 +0000)]

Improvement. Nicer handling of bit-vector not in bvxors.

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

commit | commitdiff | tree

trevor_hansen [Sun, 29 Apr 2012 10:49:41 +0000 (10:49 +0000)]

Potentiall rewriting improvement. Not sure yet.

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

commit | commitdiff | tree

trevor_hansen [Wed, 25 Apr 2012 13:49:31 +0000 (13:49 +0000)]

Fix. didn't work properly for 1 bit division.

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

commit | commitdiff | tree

trevor_hansen [Wed, 25 Apr 2012 13:40:33 +0000 (13:40 +0000)]

Improvement. Add another form of Ackermannisation. Not currently enabled.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Apr 2012 04:58:46 +0000 (04:58 +0000)]

Improvments to code used for experiments.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Apr 2012 02:09:15 +0000 (02:09 +0000)]

Changes to code for experiments.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Apr 2012 02:05:42 +0000 (02:05 +0000)]

Improvements to code for running experiments.

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

commit | commitdiff | tree

trevor_hansen [Mon, 23 Apr 2012 01:26:26 +0000 (01:26 +0000)]

Change to code for experiments.

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

commit | commitdiff | tree

trevor_hansen [Sun, 22 Apr 2012 15:43:40 +0000 (15:43 +0000)]

Change to code for running experiments.

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

commit | commitdiff | tree

trevor_hansen [Sun, 22 Apr 2012 13:15:05 +0000 (13:15 +0000)]

Change to code used for experiments.

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

commit | commitdiff | tree

trevor_hansen [Sun, 22 Apr 2012 11:52:33 +0000 (11:52 +0000)]

Improvement. Add a fast exit case to the inequalities.

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

commit | commitdiff | tree

trevor_hansen [Fri, 20 Apr 2012 01:46:09 +0000 (01:46 +0000)]

fix the build.

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

commit | commitdiff | tree

trevor_hansen [Fri, 20 Apr 2012 01:44:32 +0000 (01:44 +0000)]

Extra cpp interface constructor

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

commit | commitdiff | tree

trevor_hansen [Fri, 20 Apr 2012 01:24:47 +0000 (01:24 +0000)]

Exta utility code.

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

commit | commitdiff | tree

trevor_hansen [Fri, 20 Apr 2012 01:01:00 +0000 (01:01 +0000)]

Improvement. Change the unit propagation method to not set the model.

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

commit | commitdiff | tree

trevor_hansen [Wed, 18 Apr 2012 12:38:48 +0000 (12:38 +0000)]

Add some operations to the c-interfalce that were previously missing. Thanks to Xu Zhongxing.:

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

commit | commitdiff | tree

trevor_hansen [Tue, 17 Apr 2012 13:23:10 +0000 (13:23 +0000)]

Improvement. Adds an extra method to minisat that does unit propagation given some assignment.

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

commit | commitdiff | tree

trevor_hansen [Sun, 15 Apr 2012 06:52:35 +0000 (06:52 +0000)]

Improvmeent. Speed up the division propagator a little.

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

commit | commitdiff | tree

trevor_hansen [Fri, 13 Apr 2012 14:15:45 +0000 (14:15 +0000)]

Improvement. A cleaner bitvector addition propagator for the two input case.

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

commit | commitdiff | tree

trevor_hansen [Wed, 11 Apr 2012 12:58:24 +0000 (12:58 +0000)]

Improvement to utility code, update to new AST AIG code.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Apr 2012 07:04:29 +0000 (07:04 +0000)]

Fix build. Remove some casts that I don't need on my machine.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Apr 2012 05:07:03 +0000 (05:07 +0000)]

Testcase to check it realises neg and not are both inverse-able.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Apr 2012 04:54:59 +0000 (04:54 +0000)]

Improvement. A simplified trailing zeroes propagator.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Apr 2012 04:37:42 +0000 (04:37 +0000)]

Slightly speed up the equals propagator.

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

commit | commitdiff | tree

trevor_hansen [Tue, 10 Apr 2012 04:15:35 +0000 (04:15 +0000)]

Improvements the the code for measuring the effect of propagators.

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

commit | commitdiff | tree

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