]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
msoos [Fri, 2 Jul 2010 14:35:28 +0000 (14:35 +0000)]
Updating CryptoMiniSat2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@907
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 2 Jul 2010 12:06:37 +0000 (12:06 +0000)]
Rename the bitblaster class fron BitBlasterNew to BitBlaster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@906
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 1 Jul 2010 14:58:47 +0000 (14:58 +0000)]
Refactor, getting ready for AIGs. This does add additional code, but that code isn't currently enabled.
* Provide a base class for ToSAT. Bitblasting via ASTNodes and AIGs both implement this class.
* BBNodeManagerAIG creates AIGs that are wrapped with a BBNode object.
* BitBlastNew is now templated on the node type and the node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@905
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 29 Jun 2010 15:14:23 +0000 (15:14 +0000)]
Speedup. Generate nicer circuits for unsigned division.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@904
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Jun 2010 15:12:43 +0000 (15:12 +0000)]
Change how the counter example is built. Previously the counter example relied on specific nodes existing that wont be created when we bitblast via AIGs.
I needed to reimplement the code to print the sat model too. I didn't preserve the format. I suspect though no one is parsing it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@902
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Jun 2010 11:48:38 +0000 (11:48 +0000)]
Speedup. Add solving for xors to the bitvector solver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@901
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 28 Jun 2010 01:46:11 +0000 (01:46 +0000)]
Speedup. if (xor a b) is found, replaced a with (not b) throughout.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@900
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Jun 2010 13:52:41 +0000 (13:52 +0000)]
Speedup. Sort EQ nodes. This prevents duplicate nodes like (= 0 a), (=a 0), from being created. The bvsolver expected nodes reversed to how they are now created.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@898
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Jun 2010 10:59:46 +0000 (10:59 +0000)]
Speedup. Don't push extracts through ites. Sometimes this may be good to do. But usually not.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@896
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Jun 2010 03:38:00 +0000 (03:38 +0000)]
Default to bash shell rather than sh for some calls. The call to cat was failing on a redhat machine with an "argument too long error". Hopefully this fixes it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@895
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Jun 2010 01:52:41 +0000 (01:52 +0000)]
Speedup. Revert back to minisat's default parameters.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@892
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 27 Jun 2010 01:50:22 +0000 (01:50 +0000)]
Speedup. Flatten ands at the start of the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@891
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Jun 2010 14:59:32 +0000 (14:59 +0000)]
clean up two regression log names
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@890
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Jun 2010 08:44:09 +0000 (08:44 +0000)]
Speedups.
* The substitution map now substitutes for (IFF SYMBOL SYMBOL)
* sim.smt2 is the test case to check the above substitution is working.
* The ArrayTransformer creates fewer new nodes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@889
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 26 Jun 2010 04:16:34 +0000 (04:16 +0000)]
Speedups.
* Call topLevel simplify only if something has changed.
* If there is a symbol on the rhs put it on the lhs, which simplifies more eqns.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@888
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 25 Jun 2010 08:22:50 +0000 (08:22 +0000)]
Speedups.
* Cache the max, one and zero values inside the Create__Const() functions.
* Return a reference from the [] operator to reduce unncessary copies.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@886
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 25 Jun 2010 05:25:17 +0000 (05:25 +0000)]
Measure the difficulty of formula by using a simple function, that amongst other things counts the number of multiplications in the input. If after simplifications the difficulty has increased. Then the original formula is used instead of the not-simplified one.
This is a very rough way of performing DAG aware simplifications.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@885
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 25 Jun 2010 05:19:52 +0000 (05:19 +0000)]
Use the new method to determine whether the sub-graph contains arrays.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@884
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 25 Jun 2010 05:16:40 +0000 (05:16 +0000)]
The array transformer now respects optimisations being disabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@883
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 25 Jun 2010 05:09:28 +0000 (05:09 +0000)]
* Add containsArrayOps(..) to check if any array terms are in the graph.
* Add missing types to the typecheck function. Clean up the type check function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@881
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:36:08 +0000 (14:36 +0000)]
Fix the build.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@879
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:28:31 +0000 (14:28 +0000)]
Add a new function to replace using the substitution/solver map. It's not currently used by anything. So this checkin does nothing.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@878
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:25:59 +0000 (14:25 +0000)]
Removing duplicate files
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@877
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:21:37 +0000 (14:21 +0000)]
Remove bio tests from regressstp. They are all included in regressbio.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@876
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:16:34 +0000 (14:16 +0000)]
Adding realistic expected times to these test cases
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@875
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 14:03:37 +0000 (14:03 +0000)]
Bugfix. The script that was called by regressstp didn't record errors when some test cases failed. So I've removed it, and use the generic test runner instead. There are two differences: multiples log files are now created, and the timeout is 180 sec.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@874
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Jun 2010 11:38:31 +0000 (11:38 +0000)]
Speedup. Better cache the variables that are discovered when looking for duplicate symbols.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@872
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 15:47:01 +0000 (15:47 +0000)]
Use simplifying minisat for unit tests.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@871
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:46:24 +0000 (14:46 +0000)]
Bugfix. Simplifying minisat wasn't using the separate malloc/free routines.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@870
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:13:31 +0000 (14:13 +0000)]
Speedup/bugfix. Change how duplicate symbols are searched for. This fixed failing2.smt
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@869
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:12:16 +0000 (14:12 +0000)]
Short cut on constant evaluation
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@868
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:07:25 +0000 (14:07 +0000)]
Bugfix. Keep track of which symbols* have been deleted. Lots of them are duplicated in the map.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@867
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:06:31 +0000 (14:06 +0000)]
Don't perform simplifications when creating the substitution map. I'm not sure if this is justified, but it makes STP easier to understand. I'll check if it's useful.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@866
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:04:41 +0000 (14:04 +0000)]
Reduce memory usage. Clear out the caches from the bvsolver before calling the SAT solver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@865
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 14:02:20 +0000 (14:02 +0000)]
Fix grammar. Extra assertion.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@864
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 07:48:44 +0000 (07:48 +0000)]
Speedup. Remove some unnecessary tests.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@863
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 07:11:55 +0000 (07:11 +0000)]
Refactor. Make the TermOrder function a non-member function with the SubstitutionMap class.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@862
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 06:05:08 +0000 (06:05 +0000)]
Speedup. Shortcut if the thing we are simplifying is already a constant.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@860
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Jun 2010 03:53:02 +0000 (03:53 +0000)]
Speedup. The bvsolver now uses a reduced version of the ASTNode graph which contains nodes just for nodes where the number of descendant symbols changes.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@859
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Jun 2010 11:34:10 +0000 (11:34 +0000)]
Check for duplicate variables using a different function
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@858
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Jun 2010 06:48:44 +0000 (06:48 +0000)]
Bugfix. Variables were reported as only occuring a single time, when they actually occured multiple times.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@856
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Jun 2010 06:38:05 +0000 (06:38 +0000)]
Refactor & slight performance improvement for the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@854
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 18 Jun 2010 05:46:17 +0000 (05:46 +0000)]
Bugfix. Fix rotate_left and rotate_right to take the modulus of the shift amount. I'd misinterpreted the specification.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@852
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 16 Jun 2010 03:51:37 +0000 (03:51 +0000)]
Speedup. When printing out the counter example, don't call the toplevel print (which does lots of extra work). Instead call the low level print.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@850
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 16 Jun 2010 03:43:54 +0000 (03:43 +0000)]
Speedup. Reduce the amount of checking that the bvsolver performs.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@849
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 16 Jun 2010 03:22:39 +0000 (03:22 +0000)]
Speed up VarSeenInTerm(..) slightly.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@848
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Jun 2010 13:20:54 +0000 (13:20 +0000)]
Add some unit tests (which run when regressall is run) to check that simplifications are turning problems into TRUE or FALSE.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@846
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Jun 2010 12:34:52 +0000 (12:34 +0000)]
Bugfix. Enable the same options for when the parser is automatically detected based on filename, and when the parser is explicitly specified.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@845
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Jun 2010 07:17:05 +0000 (07:17 +0000)]
Change the properties so that SMTLIB2 format files are ignored.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@843
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Jun 2010 04:06:32 +0000 (04:06 +0000)]
Bugfix. Save the value of print counter example as per the bug report from Markus Groß
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@842
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 14 Jun 2010 03:04:47 +0000 (03:04 +0000)]
Fix regresscapi. This file wasn't checked in
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@841
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Jun 2010 14:32:53 +0000 (14:32 +0000)]
Fix the build. Add doug Lea's malloc implementation
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@838
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 13 Jun 2010 14:19:33 +0000 (14:19 +0000)]
Put the clauses of the SAT solver in a separate heap. This reduces the number of cache misses in the inner loop of the SAT solver, but increases the amount of memory STP uses.
I'm not yet sure if the extra memory usage is justified.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@837
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Jun 2010 14:55:37 +0000 (14:55 +0000)]
Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@836
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 12 Jun 2010 01:22:56 +0000 (01:22 +0000)]
Fix. I didn't update al l the function calls I should have in r832
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@835
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 15:23:37 +0000 (15:23 +0000)]
Remove no longer used bitblaster
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@834
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 15:23:04 +0000 (15:23 +0000)]
Remove the experimental bvsolver. I've copied its changes into the main bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@833
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 05:29:42 +0000 (05:29 +0000)]
* Make GetUnsignedConst a member function of ASTNode.
* In GetUnsignedConst check the position of the maximum bit only if the size is > , not >=
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@832
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 03:05:51 +0000 (03:05 +0000)]
Refactoring. Move all the substitutionmap functions into the one class.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@831
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 02:04:18 +0000 (02:04 +0000)]
This makes SimplifyTerm idempotent. My hope is that this will reduce the number of times that the toplevel function needs to be called. If a term at the bottom of the graph doesn't map to itself when SimplifyTerm is run, then all the nodes above it will need to be re-created next time SimplifyTerm is called on the graph.
This patch adds an assertion function that isn't enabled.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@830
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 11 Jun 2010 01:01:39 +0000 (01:01 +0000)]
Adds a simplification rule to replace BVANDS with zeroes at the front with a CONCAT.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@829
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Jun 2010 13:41:37 +0000 (13:41 +0000)]
bugfix. Constraints were ignored when they should have been.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@826
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Jun 2010 06:57:14 +0000 (06:57 +0000)]
Bugfix. Recursively simplify array ITES.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@824
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Jun 2010 05:06:09 +0000 (05:06 +0000)]
Add back code I removed in the last revision. Without this code fd_query_cheung2010.cvc timesout.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@823
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Jun 2010 04:00:08 +0000 (04:00 +0000)]
Bugfix. Simplify the proposition of array-ITEs. I don't simplify the "then" and "else" branch so I'm not sure if this fixes all the problems.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@821
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 9 Jun 2010 03:15:23 +0000 (03:15 +0000)]
* In the bvsolver perform cheap tests which maybe short-cut before expensive tests.
* Lazily count the number of symbols in the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@820
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Jun 2010 14:18:04 +0000 (14:18 +0000)]
Bugfix. Avoid creating cycles with the bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@817
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Jun 2010 12:52:46 +0000 (12:52 +0000)]
Bugfix. The bvsolver would replace a variable with an equation that contained that same variable. It did so because there was a special case that let it. I removed the special case.
I don't understand why the special case was there, so aren't sure if this will slow down some other instances?
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@815
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 8 Jun 2010 11:28:27 +0000 (11:28 +0000)]
Copy the cleaner new SplitEven_into_Oddnum_PowerOf2 function from bvsolverExp. I'm comparing the values from the old and new version of the function still.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@814
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 4 Jun 2010 18:11:26 +0000 (18:11 +0000)]
Last commit was wrong. Importing again CryptoMiniSat-'Cluster56'
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@813
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 4 Jun 2010 17:56:12 +0000 (17:56 +0000)]
Importing CryptoMiniSat version 'Cluster56'.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@812
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 May 2010 13:05:21 +0000 (13:05 +0000)]
Fix the method to count the number of instances in an expression. Previously it was counting no more than one.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@811
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 May 2010 13:02:47 +0000 (13:02 +0000)]
Split out the class which lazily builds the variables in terms.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@810
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 May 2010 10:40:40 +0000 (10:40 +0000)]
Small speedup in the cnf generator.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@808
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 May 2010 01:07:40 +0000 (01:07 +0000)]
Add histar to regressall. We use far far too much memory on these tests. Not sure why.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@806
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 30 May 2010 00:57:24 +0000 (00:57 +0000)]
Moving histar tests to the main test directory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@804
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 13:38:59 +0000 (13:38 +0000)]
Add my experimental BVSolver. It's much slower than the current bvsolver, but is more reliable. I'll gradually move its innovations into the main bvsolver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@803
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 13:36:55 +0000 (13:36 +0000)]
Enable upfront simplifications of terms.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@802
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 05:52:37 +0000 (05:52 +0000)]
* Make the constant evaluator a non member function. This allows the simplifying node factory to use it without holding a reference to a Simplifier object.
* Change the simplifier to use the simplifying node factory by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@801
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 05:04:50 +0000 (05:04 +0000)]
Simplifyin BVSX to CONCAT if the topmost bit of the thing being extended is known.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@800
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 04:22:11 +0000 (04:22 +0000)]
* Add a disabled-by-default option to simplify the arguments of a function first.
* Check explicitly the kind returned from some functions that create nodes to ensure the returned type is what we expect. With the simplifying node factory enabled, the type can sometimes change.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@798
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 29 May 2010 01:10:22 +0000 (01:10 +0000)]
Add a simplification so that (ite(p,5,7) <= 8) is always true is detected.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@797
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 28 May 2010 01:07:03 +0000 (01:07 +0000)]
Bugfix. If given bad input, the SMTLIB2 parser would match as much as it could then stop, without warning. It now checks that an end of file has been reached.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@796
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 27 May 2010 13:58:44 +0000 (13:58 +0000)]
* Improve the simplifications of inequalities and equalities.
* Add code to print out each of the expressions that are simplified by the bit blaster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@795
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 26 May 2010 14:32:26 +0000 (14:32 +0000)]
Implements booth recoding when bitblasting multiplication.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@793
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 05:53:15 +0000 (05:53 +0000)]
Add the "eric-tests" to regressall.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@791
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 05:50:57 +0000 (05:50 +0000)]
bugfix. Allow distinct to be used for both formulae and terms.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@790
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 02:23:57 +0000 (02:23 +0000)]
These scripts (though I don't know what they do) seem to belong with the other test generation scripts.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@787
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 02:09:23 +0000 (02:09 +0000)]
Bugfix. Rare types of array reads were causing a type-error.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@784
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 02:03:46 +0000 (02:03 +0000)]
* Letize booleans when printing back smb2lib format.
* Print back in smtlib/smtlib2 format arity > 2 and, xor, or.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@783
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 24 May 2010 01:35:39 +0000 (01:35 +0000)]
Run tests with the .smt2 extension.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@782
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 May 2010 12:55:41 +0000 (12:55 +0000)]
Fix the memory leaks in the SMTLIB2 parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@780
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 May 2010 06:36:26 +0000 (06:36 +0000)]
* fix reduce/reduce error in the smtlib2 format.
* fix dependencies of smtlib2 format in the makefile.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@779
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 23 May 2010 04:53:02 +0000 (04:53 +0000)]
The SMTLIB2 parser now accepts valid, but extremely improbable symbol names, such as: ?
It's not finished, it still leaks badly, ignores most of the commands it's sent, and doesn't allow annotations to be used.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@778
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 22 May 2010 14:08:29 +0000 (14:08 +0000)]
Fix the defintion of what a symbol is in the SMTLIB2 format.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@777
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 21 May 2010 18:23:07 +0000 (18:23 +0000)]
Use the flex options recommended by its manual.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@776
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 21 May 2010 18:21:41 +0000 (18:21 +0000)]
* Add binary & hexidecimal for smtlib2 format.
* Fix the syntax of the smtlib2 repeat function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@775
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 21 May 2010 15:55:33 +0000 (15:55 +0000)]
An initial version of an smtlib2 format parser. It has these problems:
* Leaks memory
* Doesn't allow for annotations on terms.
* Ignores the commands sent to it. It just solves the problem specified.
Other changes:
* Long options are no longer case senstive.
* If the input file ends with .smt2 or .smt the appropriate parser is selected.
* The simplifying node factory is disabled during parsing when printing back is enabled. This allows STP to be used as a better, but still low-fidelity translator between formats.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@774
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 21 May 2010 15:21:11 +0000 (15:21 +0000)]
* The bvsmod operation can now be output by the printers.
* Output the status i.e. sat, unsat if known.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@773
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 20 May 2010 03:28:27 +0000 (03:28 +0000)]
Fix the build by adding a missing function.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@772
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log