]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
vijay_ganesh [Fri, 30 Oct 2009 18:40:28 +0000 (18:40 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@372
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 30 Oct 2009 18:21:40 +0000 (18:21 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@371
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 30 Oct 2009 18:20:38 +0000 (18:20 +0000)]
added missing #ifdef CRYPTOMINISAT in STP.cpp to instantiate appropriate solver
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@370
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 22:35:01 +0000 (22:35 +0000)]
added approrpiate comments in Makefile.common
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@366
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 22:23:00 +0000 (22:23 +0000)]
added compile flags to select between the various SAT solvers (CryptoMiniSAT, MiniSAT, Simplifying MiniSAT, Unsound MiniSAT)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@365
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 18:52:13 +0000 (18:52 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@363
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 18:13:47 +0000 (18:13 +0000)]
minor edit to Makefile.in
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@362
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 17:55:56 +0000 (17:55 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@361
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 17:54:48 +0000 (17:54 +0000)]
added cryptominisat. the second time
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@360
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 17:48:26 +0000 (17:48 +0000)]
fixed the messup created in the src/sat directory
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@359
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 17:37:42 +0000 (17:37 +0000)]
some svn issues with adding cryptominisat. Hence have to remove it, and add it back
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@358
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 29 Oct 2009 17:26:51 +0000 (17:26 +0000)]
added cryptominisat code. compiles/links and runs correctly. Currently, STP does not add xor-clauses, i.e., CryptoMiniSAT runs just like MiniSAT and has the same performance.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@357
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 29 Oct 2009 03:44:47 +0000 (03:44 +0000)]
Explicitly comment out test code.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@355
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 28 Oct 2009 19:51:25 +0000 (19:51 +0000)]
did emacs indentation of all files. fixed Makefiles, and ToSAT.cpp to allow for compiling and linking with cyrptominisat
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@354
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 28 Oct 2009 17:18:47 +0000 (17:18 +0000)]
more cleanup of the deletion of various classes. For some reason delete the STPMgr class from STP class causes a segfault
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@353
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 28 Oct 2009 16:27:35 +0000 (16:27 +0000)]
improved the clearalltables() functions in various classes, and also the deletion of the pointers when STP class gets destroyed
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@352
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Oct 2009 14:55:10 +0000 (14:55 +0000)]
Update make files so that the "-j" option will work.
On my machine (see trace below), with 4 cores, make is about 3 times quicker with the -j option.
=================
~/svn/stp-trunk$ make clean > /dev/null 2>&1
~/svn/stp-trunk$ time make > /dev/null 2>&1
real 0m45.615s
user 0m41.955s
sys 0m3.152s
~/svn/stp-trunk$ clean > /dev/null 2>&1
~/svn/stp-trunk$ time make -j > /dev/null 2>&1
real 0m17.616s
user 0m44.771s
sys 0m3.744s
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@351
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Oct 2009 14:14:05 +0000 (14:14 +0000)]
Set make's default shell to bash. Previously on my machine it was bourne, which caused an error when reading the PIPESTATUS variable.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@349
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 28 Oct 2009 05:20:32 +0000 (05:20 +0000)]
Makefile bug fix. Check the CRYPTOMINISAT flag when cleaning.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@348
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 28 Oct 2009 00:14:38 +0000 (00:14 +0000)]
changed the undefined return value from MINISAT to True. Saves 30% on all regressions
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@347
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 27 Oct 2009 17:45:53 +0000 (17:45 +0000)]
added compile flags and other necessary setup for cyrptominisat.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@346
e59a4935 -1847-0410-ae03-
e826735625c1
katelman [Thu, 22 Oct 2009 20:49:16 +0000 (20:49 +0000)]
* Fixed Mac OS X compilation bug. (pull out sys/time.h from MINISAT namespace)
* Added Verilog style literals (16'd777)
* Added time out flag (-g 5, time out after 5s)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@343
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 22 Oct 2009 18:33:04 +0000 (18:33 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@342
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 22 Oct 2009 18:27:23 +0000 (18:27 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@341
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 22 Oct 2009 18:18:03 +0000 (18:18 +0000)]
Fixed a serious memory error in vc_Destroy(). Deleting the STPMgr independent of STP was causing a segfault. It has been fixed, and tested for in m32 mode and 64bit mode
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@340
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 22 Oct 2009 16:34:32 +0000 (16:34 +0000)]
added headers for CVC testcases that previously didn't have appropriate headers
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@339
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 22 Oct 2009 13:10:32 +0000 (13:10 +0000)]
Merge in changes from my branch r316 that remove redundant operations when building a counter example. This speeds up the CVC benchmarks by 10%.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@338
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 21 Oct 2009 22:19:08 +0000 (22:19 +0000)]
Changed makefiles in src/sat and scripts/Makefile.common such that m32 flag needs to be specified only in Makefile.common
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@337
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 21 Oct 2009 21:07:08 +0000 (21:07 +0000)]
added configclean target to makefile. Instead of make clean, do make configclean to remove config.info
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@336
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 21 Oct 2009 20:57:53 +0000 (20:57 +0000)]
config.info is now getting deleted during make clean
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@335
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 21 Oct 2009 13:20:42 +0000 (13:20 +0000)]
* Merge convertFormulaToCNFPosAND() from my branch. This speeds up the CVC regression tests by 25%.
* Fix. RunTimes::SendingToSAT was not stopped on one path.
* Fix unitialised values in the ArrayTransformer class.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@333
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 21 Oct 2009 05:00:53 +0000 (05:00 +0000)]
Bugfix. Off-by-one in the simplifier. This merges in the change from my branch r324
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@331
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 21 Oct 2009 04:33:15 +0000 (04:33 +0000)]
Merged in extra operations: repeat, bvcomp, bvxnor. Fixed broken BVNOR, BVNAND operations.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@329
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 21 Oct 2009 03:31:05 +0000 (03:31 +0000)]
Important BugFix. r230 introduced an off-by-one error in the left-shift circuit that ignored the value of the least significant bit of the shift amount.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@328
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 20 Oct 2009 21:28:12 +0000 (21:28 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@327
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 20 Oct 2009 21:11:34 +0000 (21:11 +0000)]
re-coded BVLE bit-blasting to start the bitblasting from the topbit (previously it was bitblasting from the bottom bit. That wasn't smart)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@326
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 20 Oct 2009 03:07:30 +0000 (03:07 +0000)]
changed the majority function for bvplus-bitblasing to clausal form. Thus improved speed by 2X
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@322
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 20 Oct 2009 02:15:35 +0000 (02:15 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@321
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 20 Oct 2009 00:44:40 +0000 (00:44 +0000)]
added an abstraction/refinement loop for clause-addition to the SAT solver
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@320
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 19 Oct 2009 18:25:20 +0000 (18:25 +0000)]
minor edits and indentation
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@319
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 18 Oct 2009 11:34:38 +0000 (11:34 +0000)]
Speed up grep0084.stp.cvc & grep0117.stp.cvc, by reducing unnecessary memory copying in the CNF generator
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@313
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:24:56 +0000 (18:24 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@312
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:08:59 +0000 (18:08 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@311
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 16 Oct 2009 18:06:45 +0000 (18:06 +0000)]
changed some files to fit into 80 characters terminal
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@310
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 22:45:29 +0000 (22:45 +0000)]
Cleaned up the printing of bitblasted formula and clauses. This will help me figure out how efficient the bitblaster/cnf translator are
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@308
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 21:52:58 +0000 (21:52 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@306
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 15 Oct 2009 21:52:37 +0000 (21:52 +0000)]
marked completed tasks in the task-list
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@305
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 20:27:36 +0000 (20:27 +0000)]
formatted using gnu style
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@304
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 19:53:48 +0000 (19:53 +0000)]
All userdefined flags are now local to STPManager. not global anymore
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@303
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 14 Oct 2009 17:05:17 +0000 (17:05 +0000)]
code indented using emacs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@302
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 13 Oct 2009 19:12:36 +0000 (19:12 +0000)]
push/pop now working through the c_interface. Clearalltabes has been implemented correctly and tested
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@300
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 13 Oct 2009 15:44:00 +0000 (15:44 +0000)]
added cleartables for each of the big classes
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@299
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 21:12:00 +0000 (21:12 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@298
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 20:58:21 +0000 (20:58 +0000)]
removed ASTUtil.h and merged with UsefulDefs.h
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@297
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 12 Oct 2009 20:48:11 +0000 (20:48 +0000)]
replaced hash_map/hash_set with defines HASHMAP and HASHSET resp.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@296
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 02:09:52 +0000 (02:09 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@292
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 02:06:21 +0000 (02:06 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@291
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 01:41:31 +0000 (01:41 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@290
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 01:31:34 +0000 (01:31 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@289
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:57:35 +0000 (00:57 +0000)]
renamed BeevMgr to STPMgr
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@288
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:12:49 +0000 (00:12 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@287
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:12:23 +0000 (00:12 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@286
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:11:39 +0000 (00:11 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@285
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 11 Oct 2009 00:07:43 +0000 (00:07 +0000)]
big reorganization almost complete. I believe there is a slight slowdown.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@284
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 6 Oct 2009 01:16:35 +0000 (01:16 +0000)]
moved all LET-variables related stuff into a separate class
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@282
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 5 Oct 2009 23:10:08 +0000 (23:10 +0000)]
reorganized ToCNF
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@281
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 5 Oct 2009 17:28:56 +0000 (17:28 +0000)]
more reorganization. introduced STPManager directory, and move BeevMgr class to it
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@280
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 22:37:12 +0000 (22:37 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@276
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 22:27:30 +0000 (22:27 +0000)]
removed symbol table from AST
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@275
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:39:34 +0000 (21:39 +0000)]
more AST reorganization
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@274
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:36:33 +0000 (21:36 +0000)]
more AST reorganization
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@273
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 21:19:59 +0000 (21:19 +0000)]
moved function defintions for AST classes to appropriate cpp files
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@272
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 20:08:29 +0000 (20:08 +0000)]
massiv code cleanup. Created separate files for ASTNode, ASTInternal, ASTInterior, ASTSymbol, ASTBVConst
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@271
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 2 Oct 2009 15:21:03 +0000 (15:21 +0000)]
added logs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@270
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 1 Oct 2009 18:08:32 +0000 (18:08 +0000)]
massive changes. Added a LESSBYTES_PER_NODE option. Cuts down the bytesize of nodes by more than 20%
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@269
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 30 Sep 2009 23:14:43 +0000 (23:14 +0000)]
shaved off 4 bytes from each ASTInternal node
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@268
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 29 Sep 2009 16:03:40 +0000 (16:03 +0000)]
fixed bug in c_interface bvconstExprFromInt
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@266
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 28 Sep 2009 18:14:38 +0000 (18:14 +0000)]
changed the var decay. It improved performace
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@265
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 27 Sep 2009 22:35:22 +0000 (22:35 +0000)]
added checks for bvconst construction. checks if the n_bits is adequate to represent the constant
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@262
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 27 Sep 2009 19:26:38 +0000 (19:26 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@261
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 26 Sep 2009 19:37:00 +0000 (19:37 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@258
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 26 Sep 2009 01:32:37 +0000 (01:32 +0000)]
minor
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@257
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 25 Sep 2009 20:13:02 +0000 (20:13 +0000)]
added more tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@256
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 24 Sep 2009 14:46:50 +0000 (14:46 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@253
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 24 Sep 2009 13:46:11 +0000 (13:46 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@252
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 24 Sep 2009 10:47:08 +0000 (10:47 +0000)]
Different flex options as provided by Peter Collingbourne.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@251
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 23 Sep 2009 02:41:03 +0000 (02:41 +0000)]
* get biosat-rna.cpp compiling on my machine.
* add const to some char* in the c_interface to remove compiler warnings.
* %ld -> %llu to remove compiler warnings in tests.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@249
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 22 Sep 2009 16:46:44 +0000 (16:46 +0000)]
fixed the regression scripts so that we can run them one after another with one command
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@248
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 22 Sep 2009 00:43:54 +0000 (00:43 +0000)]
added new testing perl script. minor edits to Makefiles.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@247
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 23:42:04 +0000 (23:42 +0000)]
All fixed. RNA example is running again. I had introduced some Abstraction-refinement code in AST.h. It seems to have pushed the system to limits of memory consumption
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@246
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 21:34:38 +0000 (21:34 +0000)]
added biosat-rna.cpp file. It is crashing now. Previously it was running smoothly in 133 seconds
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@245
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 21 Sep 2009 18:26:39 +0000 (18:26 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@244
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Sep 2009 15:47:09 +0000 (15:47 +0000)]
* Don't allow creation of zero-width bitvector literals. Previously bv0[0] would parse via the SMTLIB input language
* If optimisations were disabled, sign_extend[0], would segfault in the bitblaster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@243
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 20 Sep 2009 13:46:04 +0000 (13:46 +0000)]
* Bug-fix. Prior checkin broke zero_extend by greater than the machine's unsigned size. So zero_extend[100] would fail.
* Remove old code from the parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@241
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 19 Sep 2009 13:40:13 +0000 (13:40 +0000)]
Remove BVZX. Bit vector zero extend is now replaced by a prepend with a zero bitvector at parse time.
The simplification rules over concatentations are better than those that were over BVZX.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@240
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 15:40:50 +0000 (15:40 +0000)]
* -t times how long sending the clauses to the SAT solver takes.
* Remove unreachable code in the loop sending clauses to the SAT solver.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@239
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 04:54:11 +0000 (04:54 +0000)]
* Add back -m32. All should now make at 32-bit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@237
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 17 Sep 2009 04:37:49 +0000 (04:37 +0000)]
* Add -m32 flag to c-api-tests to get it compiling
* -t now tracks the bvsolver, and the substitution mapper (which sometimes takes a freakishly large amount of time).
* SimplifyCaches are no longer cleared at the start of topLevel simplify. Sometimes there is good stuff in there.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@236
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 16 Sep 2009 22:23:59 +0000 (22:23 +0000)]
minor edits to scrips/Makefile.common
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@235
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 16 Sep 2009 22:23:25 +0000 (22:23 +0000)]
minor edits to AST/Makefile
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@234
e59a4935 -1847-0410-ae03-
e826735625c1
projects / francis / stp.git / log