]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
vijay_ganesh [Sat, 5 Dec 2009 03:12:34 +0000 (03:12 +0000)]
lots of changes aimed at CryptoMiniSAT2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@455
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 4 Dec 2009 10:36:39 +0000 (10:36 +0000)]
Updating to cryptominisat2 git revision
63f0b6f7e4927759643c97913060c37f8ae4c82a
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@454
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 4 Dec 2009 10:36:20 +0000 (10:36 +0000)]
Updating CryptoMiniSat to r519. Should fix problems with xor-conglomeration, and should also free all memory
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@453
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 4 Dec 2009 00:53:54 +0000 (00:53 +0000)]
reverted back the changes
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@452
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 4 Dec 2009 00:09:09 +0000 (00:09 +0000)]
played with cryptominisat parameters to improve performance
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@451
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 3 Dec 2009 23:30:54 +0000 (23:30 +0000)]
more xor-clausing for equality and BVLE/BVLT etc
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@450
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Wed, 2 Dec 2009 16:34:56 +0000 (16:34 +0000)]
Disabling var-replacer feature of CryptoMiniSat to allow for programmable solver
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@449
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Wed, 2 Dec 2009 16:27:28 +0000 (16:27 +0000)]
Updating CryptoMiniSat2 to r504, fixing all known bugs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@448
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 2 Dec 2009 16:18:36 +0000 (16:18 +0000)]
removed a broken test
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@447
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 2 Dec 2009 00:52:09 +0000 (00:52 +0000)]
added -march=native as compile option
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@446
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 23:47:30 +0000 (23:47 +0000)]
Revert "CryptoMiniSat2 is using the same MTL and MTRand directory as that of"
This reverts commit
fe8e65ee4998cf999b2dedecd5dabcad7192579c .
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@445
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 23:46:19 +0000 (23:46 +0000)]
Revert "Sorry, Solver.h's #include directive wasn't cleaned from 'MTRand/' in last commit"
This reverts commit
2ca9fce7e56faf8bc26285597a323f9dbe1e6b00 .
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@444
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 23:14:57 +0000 (23:14 +0000)]
Updating CryptoMiniSat2 to r494. The only difference between this
version and the version in SVN is that performReplace() is not called
here. The reasons for this are:
1) performReplace() is at the moment buggy when MiniSat is used as a
library
2) For a programmable solver, we need to have all variables to
propagating at all times, thus we cannot accept to have certain
variables acting as more than one (for which performReplace is
used)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@443
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 22:54:57 +0000 (22:54 +0000)]
Sorry, Solver.h's #include directive wasn't cleaned from 'MTRand/' in last commit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@442
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 1 Dec 2009 22:41:21 +0000 (22:41 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@441
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 1 Dec 2009 22:40:55 +0000 (22:40 +0000)]
commented out clause dumping during debug-printing
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@440
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 22:35:14 +0000 (22:35 +0000)]
CryptoMiniSat2 is using the same MTL and MTRand directory as that of
CryptoMiniSat1. This is made explicit by the Makefile's -I directives.
Therefore, there is no need to have it twice in the source tree. Also,
some files in CryptoMiniSat2 have been changed to have 'mtl/' in front
of their #include directives. This was superflous, as the Makefile
already -I includes the ../cryptominisat/mtl and ../cryptominisat/MTRand
directories in the search path.Effectively, with 'mtl' directory in,
and the #include 'mtl/X.h', it was compiler-implementation specific
which file was included (either cryptominisat/mtl/X.h or
cryptominisat2/mtl/X.h), therefore potentially making debugging next to
impossible and the build fragile in the future (if ever the two mtl
directories will be different)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@439
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 22:33:02 +0000 (22:33 +0000)]
Reverting commit no r435. Adding 'using namespace std' is dangerous as
sort() is defined by both the std and the mtl libraries.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@438
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 1 Dec 2009 22:31:09 +0000 (22:31 +0000)]
Fixing problem with CRYPTOMINSAT2 from an STP point of view. simplify() does not need to be called before solve() in either CRYPTOMINISAT1 or 2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@437
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 1 Dec 2009 22:26:03 +0000 (22:26 +0000)]
added some more crypto examples
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@436
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 1 Dec 2009 21:17:04 +0000 (21:17 +0000)]
fixed compile error on certain gcc versions. added using namespace std in Solver.cpp
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@435
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 1 Dec 2009 18:43:20 +0000 (18:43 +0000)]
added crypto tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@434
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 30 Nov 2009 19:50:46 +0000 (19:50 +0000)]
fixed compile/link issues with cryptominisat version 2.0
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@433
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 30 Nov 2009 18:47:08 +0000 (18:47 +0000)]
Updating cryptominsat2 to revision r483. Multiple performance bugs fixed, glucose solver has been partially imported, and a memory leak has been fixed -- approx. 600 lines changed
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@432
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 27 Nov 2009 10:26:24 +0000 (10:26 +0000)]
MTRand directory was not included in the search path for the compiler when compiling CryptoMiniSat ver. 1
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@431
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 27 Nov 2009 10:26:14 +0000 (10:26 +0000)]
CryptoMiniSat2's Makefile had the same mistake as the other CryptoMiniSat's original Makefile. Corrected
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@430
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 27 Nov 2009 10:26:02 +0000 (10:26 +0000)]
Adding Cryptominisat Version 2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@429
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 26 Nov 2009 19:22:52 +0000 (19:22 +0000)]
Significant good changes to SAT makefiles by Mate. Issues with STP library creation. Now Fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@428
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 26 Nov 2009 00:32:16 +0000 (00:32 +0000)]
Removing template.mk completely, and replacing it with proper Makefile-s in minisat's 'core' and 'simp' directory
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@427
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 26 Nov 2009 00:31:35 +0000 (00:31 +0000)]
cryptominisat's Makefile had its 'clean' missing
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@426
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 26 Nov 2009 00:18:00 +0000 (00:18 +0000)]
Renaming of cryptominisat-files, and creating a proper Makefile for
crytominisat
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@425
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 25 Nov 2009 20:12:47 +0000 (20:12 +0000)]
added variable right shift to the CVC parser
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@424
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 24 Nov 2009 21:05:54 +0000 (21:05 +0000)]
added symbolic link in include/stp/c_interface.h to the appropriate c_interface.h
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@423
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 20 Nov 2009 22:10:50 +0000 (22:10 +0000)]
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@420
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 20 Nov 2009 18:57:33 +0000 (18:57 +0000)]
minor edit to the Clausal abstraction limit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@419
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 19 Nov 2009 20:54:25 +0000 (20:54 +0000)]
fixed some bugs in the user-guided refinement implementation
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@418
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 19 Nov 2009 17:53:17 +0000 (17:53 +0000)]
minor edits to the user-guided absrefine example
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@417
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 18 Nov 2009 23:07:17 +0000 (23:07 +0000)]
added a testcase for userguided refinement
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@414
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 18 Nov 2009 21:18:56 +0000 (21:18 +0000)]
added ability to generate xor-clauses with negation on top
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@413
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 18 Nov 2009 20:20:19 +0000 (20:20 +0000)]
userguided abstraction-refinement is now at the toplevel
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@412
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 17 Nov 2009 19:28:14 +0000 (19:28 +0000)]
added an experimental user-guided abstraction-refinement loop
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@411
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 17 Nov 2009 02:52:22 +0000 (02:52 +0000)]
user-defined abstraction refinement basic functions in place. More thorough testing TBD
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@410
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 16 Nov 2009 23:13:05 +0000 (23:13 +0000)]
added code to facilitate user-guided abstraction-refinement
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@409
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 16 Nov 2009 17:19:16 +0000 (17:19 +0000)]
minor edits to README
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@408
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 16 Nov 2009 17:13:31 +0000 (17:13 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@407
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 16 Nov 2009 17:06:56 +0000 (17:06 +0000)]
added info about installation regression in README
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@406
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 16 Nov 2009 17:01:45 +0000 (17:01 +0000)]
added a very basic regression so that users can check their installations
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@405
e59a4935 -1847-0410-ae03-
e826735625c1
xiw [Sat, 14 Nov 2009 08:47:40 +0000 (08:47 +0000)]
fixed a crash in parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@404
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 13 Nov 2009 21:23:41 +0000 (21:23 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@403
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 13 Nov 2009 19:10:14 +0000 (19:10 +0000)]
fixed the flex-related bug
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@402
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 13 Nov 2009 18:41:12 +0000 (18:41 +0000)]
more deadcode eliminated
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@401
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 13 Nov 2009 01:19:00 +0000 (01:19 +0000)]
removed some deadcode relating to previous versions of cleartable and clearcache functions
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@400
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 12 Nov 2009 23:21:37 +0000 (23:21 +0000)]
fixed a bug in the CVC parser. It was allowing the user to input only assertions, and then segfaulting because there was no query.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@399
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 12 Nov 2009 17:29:35 +0000 (17:29 +0000)]
first round of cryptominisat integration is complete
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@398
e59a4935 -1847-0410-ae03-
e826735625c1
katelman [Thu, 12 Nov 2009 05:31:15 +0000 (05:31 +0000)]
Fixed a couple of bugs in the way that we do clause generation for
Cryptominisat.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@396
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 9 Nov 2009 16:52:56 +0000 (16:52 +0000)]
calling CRYPTOMINISAT Simplify() before calling Solve()
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@395
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 9 Nov 2009 16:28:44 +0000 (16:28 +0000)]
fixed some slowdowns
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@394
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 9 Nov 2009 03:58:30 +0000 (03:58 +0000)]
Revert to version #390, didn't mean to checkin this change.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@393
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 9 Nov 2009 03:55:50 +0000 (03:55 +0000)]
Option currently disabled. To not use Tseitin variables as decision variables. On problems that spend the majority of time in the SAT solver, this gives 35% improved performance. I don't yet understand how it interacts with the CNF bucketisation, so until then won't enable it by default.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@392
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sun, 8 Nov 2009 14:55:30 +0000 (14:55 +0000)]
Add extra dependencies required for parallel build.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@391
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 6 Nov 2009 21:20:09 +0000 (21:20 +0000)]
minor changes
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@390
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 6 Nov 2009 16:46:52 +0000 (16:46 +0000)]
fixed a memory-leak introduced during the process of fixing memory-leaks
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@389
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Nov 2009 13:12:40 +0000 (13:12 +0000)]
Fix memory leaks triggered by capi testcase 15 (x.c).
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@388
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Nov 2009 12:45:37 +0000 (12:45 +0000)]
* Fix memory leaks in the c-api for testcases 11 & 20. However, testcase 5 is now broken and is commented out.
* If Valgrind is installed in the path, test cases 3,11&20 will run under Valgrind. Those test cases neither leak nor use unitialised memory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@387
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Nov 2009 05:13:37 +0000 (05:13 +0000)]
Read the global STPManager in cleanup(), rather than a pointer to it.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@386
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Nov 2009 05:11:26 +0000 (05:11 +0000)]
Reduce the number of iterations that the leak checking tests perform.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@385
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Fri, 6 Nov 2009 05:10:00 +0000 (05:10 +0000)]
Bugfix. Add explicit delete of expressions to test case.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@384
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 5 Nov 2009 19:41:46 +0000 (19:41 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@383
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 5 Nov 2009 19:41:17 +0000 (19:41 +0000)]
added xor clause adding to cryptominisat. still being debugged
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@382
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 Nov 2009 14:10:20 +0000 (14:10 +0000)]
Bugfixes.
* Create a copy of the output of vc_bvType(,). The copies persists until vc_destroy() is called when they are cleaned up automatically.
* Explicitly delete an expression in on of our test cases.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@381
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 Nov 2009 12:50:10 +0000 (12:50 +0000)]
Bugfix. memory leak.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@380
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 4 Nov 2009 12:40:39 +0000 (12:40 +0000)]
Bugfix. A leak in simplifier.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@379
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 3 Nov 2009 19:57:29 +0000 (19:57 +0000)]
added fix so that STP can read back its SMTLIB printout
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@378
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 3 Nov 2009 17:17:59 +0000 (17:17 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@377
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 3 Nov 2009 17:14:55 +0000 (17:14 +0000)]
added ability to parse SMT files from the c_interface
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@376
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Tue, 3 Nov 2009 14:41:00 +0000 (14:41 +0000)]
* Add the leak.c test which is currently failing.
* Set the virtual memory limit low when checking for leaks.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@375
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 3 Nov 2009 02:09:28 +0000 (02:09 +0000)]
bucketization of clauses added, and tested
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@374
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 3 Nov 2009 00:34:22 +0000 (00:34 +0000)]
Added funcion in CallSAT.cpp to bucketize the clauselist
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@373
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log