]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Sun, 28 Feb 2010 11:29:00 +0000 (11:29 +0000)]
Testcase and temporary bugfix for an interface problem reported by Alvin Cheung.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@619
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 25 Feb 2010 12:22:20 +0000 (12:22 +0000)]
Updates to the "bench" printer.
* True and False are now output as respectively vdd and gnd.
* For functions like 'and' with lots of arguments, the height is not logaritmic in the number of arguments, not linear.
* Better caching, much faster.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@617
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 22 Feb 2010 11:49:47 +0000 (11:49 +0000)]
* The bench printer prints out bitblasted formula which can be loaded by the ABC logic synthesis tool.
* The GDL printer prints out graphs which can be laid out by aiSee3.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@616
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 13 Feb 2010 12:20:28 +0000 (12:20 +0000)]
Bugfix. Bitblasting failed when a BVSX didn't increase the length
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@613
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Thu, 4 Feb 2010 12:06:51 +0000 (12:06 +0000)]
Apply patch to fix Macos compilation provided by Mieszko Lis.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@588
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 1 Feb 2010 12:51:01 +0000 (12:51 +0000)]
NodeFactory classes that are used to build functions. The HashingNodeFactory uses existing code to perform structural hashing. The SimplifyingNodeFactory applies straight forward simplifications. The TypeCheck wraps around another node factory to type check each node after it's created.
Classes that currently take an STPManager as a parameter, but just use it to create nodes will over time be changed to instead take a node factory.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@581
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Thu, 21 Jan 2010 21:47:07 +0000 (21:47 +0000)]
fixed an important problem with YACC STACK DEPTH. It was too low previously. Now fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@560
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Wed, 20 Jan 2010 14:06:10 +0000 (14:06 +0000)]
Bugfix. revision 558 broke all the solvers except for cryptominisat
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@559
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 18 Jan 2010 02:36:41 +0000 (02:36 +0000)]
Bugfix. revision 556 broke cryptominisat. If cryptominisat was enabled, the xor data structure was deleted twice.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@558
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 18 Jan 2010 02:02:22 +0000 (02:02 +0000)]
Fix some leaks
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@556
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Mon, 11 Jan 2010 15:39:52 +0000 (15:39 +0000)]
Bugfix. Simplifying minisat not setting a return code as expected. Copied from my branch r517.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@552
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sun, 10 Jan 2010 21:07:20 +0000 (21:07 +0000)]
BitBlast.cpp: Was generating XOR-clauses by default since this is very good for CryptoMiniSAT2. However, forgot put it under flag. Now corrected.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@551
e59a4935 -1847-0410-ae03-
e826735625c1
vijay_ganesh [Sat, 9 Jan 2010 23:05:26 +0000 (23:05 +0000)]
minor modification to Makefile.common to isolate some memory blowup problems
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@550
e59a4935 -1847-0410-ae03-
e826735625c1
xiw [Thu, 7 Jan 2010 10:31:54 +0000 (10:31 +0000)]
avoid UINT32_MAX redefinition warning
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@549
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 25 Dec 2009 19:56:50 +0000 (19:56 +0000)]
Updating CMS2 to r686
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@543
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 24 Dec 2009 15:04:04 +0000 (15:04 +0000)]
Updating to CMS2 r 685, fixing some bugs and doing some explicit casting on std::min
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@542
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Tue, 22 Dec 2009 18:41:33 +0000 (18:41 +0000)]
Updating CMS2 to r681, fixing multiple bugs, and adding some polish
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@539
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Wed, 16 Dec 2009 16:11:49 +0000 (16:11 +0000)]
Updating CryptoMiniSat2 to r656
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@520
e59a4935 -1847-0410-ae03-
e826735625c1
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
projects / francis / stp.git / log