]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
vijay_ganesh [Mon, 7 Dec 2009 01:32:20 +0000 (01:32 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@470
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 01:19:11 +0000 (01:19 +0000)]
cryptominisat2 is now the official SAT solver of STP
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@468
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 6 Dec 2009 21:49:20 +0000 (21:49 +0000)]
added option to that allows STP to give randomized answers to queries
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@467
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Sun, 6 Dec 2009 17:28:40 +0000 (17:28 +0000)]
Updating CryptoMiniSat to SVN r561, fixing a log of bugs
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@466
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 23:12:21 +0000 (23:12 +0000)]
changed the way BVDIV is bitblasted
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@465
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 22:51:17 +0000 (22:51 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@464
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 22:41:40 +0000 (22:41 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@463
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 22:38:15 +0000 (22:38 +0000)]
added one more test in stp-tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@462
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 22:26:20 +0000 (22:26 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@461
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 21:49:12 +0000 (21:49 +0000)]
compressed some of the larger bio tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@460
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 20:31:48 +0000 (20:31 +0000)]
added some small bio examples
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@459
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 19:14:12 +0000 (19:14 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@458
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 19:13:04 +0000 (19:13 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@457
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 5 Dec 2009 03:22:43 +0000 (03:22 +0000)]
added lots of synthesis tests, and crypto tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@456
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log