]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
trevor_hansen [Tue, 24 Jan 2012 04:26:37 +0000 (04:26 +0000)]
Improvement. Add the ability to set a soft timeout via the c_interface. You specify the number of milliseconds that you want STP to run for.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1520
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 24 Jan 2012 01:25:17 +0000 (01:25 +0000)]
Clean up. I think this is just a refactor, but aren't sure. The c_interface set removewrites to true sometimes. It was the only place in the code that set it...
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1519
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 24 Jan 2012 00:49:15 +0000 (00:49 +0000)]
Refactor. Automatically layout code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1518
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 24 Jan 2012 00:48:40 +0000 (00:48 +0000)]
Refactor. Rename parserinterface to cpp_interface.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1517
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log