]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Wed, 16 Dec 2009 05:33:31 +0000 (05:33 +0000)]
Fix simplifying minisat. Previously when the SIMP flag was set, simplifying minisat would not be used. The simplifying solver derived from Minisat, but the solve() method etc. of the base class were not virtual.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@515
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Dec 2009 22:41:24 +0000 (22:41 +0000)]
accidental Makefile.common commit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@505
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Dec 2009 22:36:41 +0000 (22:36 +0000)]
branched STP into a programmable branch. Add programmable SAT code to cryptominisat2 dir. svn removed previous code in that dir
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@504
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Dec 2009 00:43:53 +0000 (00:43 +0000)]
fixed erroneous checkin. reverted NOT functionality back
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@503
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Fri, 11 Dec 2009 00:27:54 +0000 (00:27 +0000)]
converting NOT(a) into XOR(a, true). Helps with bio. Breaks test000013.cvc
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@502
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 10 Dec 2009 19:57:04 +0000 (19:57 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@501
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 10 Dec 2009 19:39:18 +0000 (19:39 +0000)]
added some relatively hard bio examples
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@500
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 10 Dec 2009 19:13:48 +0000 (19:13 +0000)]
Set RenameAllSibs Flag to false. It was slowing down bio
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@499
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 10 Dec 2009 16:38:33 +0000 (16:38 +0000)]
made -fPIC and -march=native optional
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@498
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 10 Dec 2009 15:19:30 +0000 (15:19 +0000)]
Updating CryptoMiniSat2 to r614. dynamicRestart is now automatic, and turns off gauss automatically. Cleanclauses and performReplace are now used only when they seem to provide benefit. Gauss depth is now set to 100 in STP.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@497
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Dec 2009 19:45:20 +0000 (19:45 +0000)]
added SAT verbosity to statistics option
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@496
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Dec 2009 18:02:28 +0000 (18:02 +0000)]
added -fPIC flag for Java programs that want to use STP as a library
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@495
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Wed, 9 Dec 2009 02:11:49 +0000 (02:11 +0000)]
fixed the bug in CNF translation that caused test000013.cvc to slow down
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@494
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 23:59:37 +0000 (23:59 +0000)]
good options of CMS2 set
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@493
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 23:19:23 +0000 (23:19 +0000)]
fixed compile error on MacOS X
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@492
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 22:55:51 +0000 (22:55 +0000)]
clausal bucketing back in business
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@491
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 22:32:26 +0000 (22:32 +0000)]
completely got rid of abs-refine at boolean clausal level
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@490
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 20:50:21 +0000 (20:50 +0000)]
fixed a small bug in cryptominisat2
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@489
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 8 Dec 2009 20:28:16 +0000 (20:28 +0000)]
Updating CryptoMiniSat to r594. dynamicRestarts is now an option
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@488
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 20:05:44 +0000 (20:05 +0000)]
minor edits
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@487
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 18:05:26 +0000 (18:05 +0000)]
completed the cnf dumping feature. it works
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@486
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 17:24:48 +0000 (17:24 +0000)]
added cnf dumping facility
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@485
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Tue, 8 Dec 2009 17:04:05 +0000 (17:04 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@484
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 8 Dec 2009 13:31:11 +0000 (13:31 +0000)]
Updating CryptoMiniSat to r586. Need to call 'void needLibraryCNFFile(const char* fileName);' once exactly after Solver object creation to have CNF file output from library calls
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@483
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 7 Dec 2009 23:39:27 +0000 (23:39 +0000)]
Updating CryptoMiniSat to r579, fixing a small bug, and adding a minor performance-increasing patch
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@481
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 21:42:45 +0000 (21:42 +0000)]
XOR output for ITE
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@480
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 7 Dec 2009 20:03:13 +0000 (20:03 +0000)]
Updating CryptoMiniSat2 to r577
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@479
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 19:18:37 +0000 (19:18 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@478
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 17:46:17 +0000 (17:46 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@477
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 17:45:45 +0000 (17:45 +0000)]
minor edit
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@476
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Mon, 7 Dec 2009 17:28:21 +0000 (17:28 +0000)]
added a regression script for synthesis tests
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@475
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 7 Dec 2009 15:48:56 +0000 (15:48 +0000)]
Updating CryptoMiniSat to r565. Should solve the problem with performReplace failing. It also brings a bit of speedup and a cleaner performReplace::replace_set() code for a cleaner (thus easier-to-debug) code
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@474
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log