]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Fri, 9 Jul 2010 08:28:46 +0000 (08:28 +0000)]
Add the option to exit after generating the CNF. Currently only works for bit-vectors (which don't have abstraction refinement).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@942
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 9 Jul 2010 08:25:48 +0000 (08:25 +0000)]
Bugfix. If a new-line occured in a string literal, it wasn't matched by the lexer, so would be printed out to the console.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@941
e59a4935 -1847-0410-ae03-
e826735625c1
petercol [Thu, 8 Jul 2010 17:12:36 +0000 (17:12 +0000)]
Introduce vc_setInterfaceFlags function
This patch adds a vc_setInterfaceFlags function to the C interface
with one possible flag, EXPRDELETE, which is set by default. The flag
controls whether the C interface deletes types and integer constant
expressions at vc_Destroy time. It is intended that clients which
perform their own memory management of these objects will be able to
clear this flag.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@940
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:16:17 +0000 (05:16 +0000)]
Fix some small leaks when performing division by zero, and in the smtlib1 parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@939
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:14:38 +0000 (05:14 +0000)]
Only run the bvsolver if optimisations have been enabled. The bvsolver relies on optimisations being performed for correctness.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@938
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 8 Jul 2010 05:10:55 +0000 (05:10 +0000)]
Fix the unit test script:
* To not explicitly call simplifying minisat (which isn't an option if compiled with cms).
* To remove comments and blank lines (which are introduced by AIG's conversion).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@937
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 13:33:08 +0000 (13:33 +0000)]
Bugfix. Remove a null pointer reference.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@936
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 13:17:57 +0000 (13:17 +0000)]
Simplify (bvdiv x x ) to one. Likewise for the other multiplication like operations.
Other changes are for constant bit propagation (aren't active yet).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@935
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:51:08 +0000 (07:51 +0000)]
Fix the building of the stp library.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@934
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:37:55 +0000 (07:37 +0000)]
Fix the build.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@933
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 7 Jul 2010 07:33:58 +0000 (07:33 +0000)]
Neaten up the code for constant bit propagation. Note this code doesn't run by default, so this patch shouldn't change anything.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@932
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 14:38:52 +0000 (14:38 +0000)]
Bugfix. Fix a check to ensure that the type of nodes doesn't change for the worst.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@931
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 05:03:02 +0000 (05:03 +0000)]
* Interface changes for constant bit propagation. Not currently enabled.
* Add code to bitblast etc. for bvzx. BVZX can be created via the interface, and might not be simplified out before reaching the bitblaster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@930
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 01:35:43 +0000 (01:35 +0000)]
Fix. stp.a didn't have necessary cbitp file included. Thanks to Peter Collingbourne for the patch.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@929
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 01:34:44 +0000 (01:34 +0000)]
Fix. The unit tests expect the cnf's to be called output_*.cnf. If going to CNF via AIGs it was called output.cnf
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@928
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 6 Jul 2010 01:33:40 +0000 (01:33 +0000)]
Revert. In r915 I removed the default -m32 flag by accident.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@927
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 5 Jul 2010 13:26:19 +0000 (13:26 +0000)]
More getting ready for constant bit propagation. This code doesn't run, so nothing should change.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@926
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 5 Jul 2010 09:27:00 +0000 (09:27 +0000)]
CryptoMiniSat can now be built
How to build CryptoMS:
1) install cmake
2) go to the "src/sat/cryptominisat2/" directory
3) create new dir: "mkdir build"
4) go to new dir: "cd build"
5) type "cmake ../"
6) type "make"
7) the "cryptominisat" binary is now in the directory
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@925
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 5 Jul 2010 08:48:57 +0000 (08:48 +0000)]
For low-cutoff speed reasons, it's best not to subsume learnts
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@924
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 5 Jul 2010 04:43:52 +0000 (04:43 +0000)]
Add the interface code for constant bit propagation. This isn't all of the code, just the code required to interface with the bit blaster.
This code isn't called. So this patch doesn't change STP at all.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@923
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Sun, 4 Jul 2010 18:17:55 +0000 (18:17 +0000)]
Cleaning up some bugs in CryptoMS
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@920
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 4 Jul 2010 12:23:07 +0000 (12:23 +0000)]
Free the memory allocatated to the AIGs before SAT solving.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@919
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 4 Jul 2010 08:25:47 +0000 (08:25 +0000)]
Tiny speedup. Generate the encoding of multiplication slightly more efficiently.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@918
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 4 Jul 2010 07:58:00 +0000 (07:58 +0000)]
I didn't enable capturing of quick statistics (the -t flag) for the time spent bitblasting when using AIGS.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@917
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 4 Jul 2010 07:45:38 +0000 (07:45 +0000)]
Bugfix. The SMTLIB2 defines the outer bars (if present) to not be part of the symbol name.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@916
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 4 Jul 2010 05:42:13 +0000 (05:42 +0000)]
Get cryptominisat2 compiling:
* Add a cutdown copy of the Boost library.
* Comment out most of the Cryptominisat2 custom code. I've changed the IFDEFs to cryptominisat__2, which leaves the code in, but which isn't defined.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@915
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 3 Jul 2010 13:15:31 +0000 (13:15 +0000)]
Bitblast formula that don't contain arrays into and-inverter graphs. This uses the AIG implementation provided by the ABC package.
This has some advantages:
* The AIG nodes are smaller than our ASTNodes, so it uses less memory.
* The CNFs generated by ABC are smaller, so generally solving is quicker.
Some notes:
* I haven't made the CNF converter incremental, so bitblasting to AIGs is only enabled for bit-vector problems (which STP bitblasts eagerly).
* AIG re-writing isn't enabled yet.
* From prior experience some big problems fail in CNF encoding. All of our test cases pass though.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@913
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 2 Jul 2010 14:58:09 +0000 (14:58 +0000)]
Correcting small bug in CMS2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@912
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 2 Jul 2010 14:49:00 +0000 (14:49 +0000)]
Updating CMS2 to get rid of a small bug
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@911
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 2 Jul 2010 14:36:16 +0000 (14:36 +0000)]
Removing trailing code related to pools' #ifdefs in CryptoMS
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@910
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 2 Jul 2010 14:36:03 +0000 (14:36 +0000)]
Further updating of CryptoMiniSat2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@909
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 2 Jul 2010 14:35:49 +0000 (14:35 +0000)]
Updating CryptoMiniSat2 to fix some minor bugs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@908
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log