git.unchartedbackwaters.co.uk Git - francis/stp.git/log

]> git.unchartedbackwaters.co.uk Git - francis/stp.git/log

projects / francis / stp.git / log

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

commit | commitdiff | tree

trevor_hansen [Tue, 2 Mar 2010 12:53:46 +0000 (12:53 +0000)]

* When outputting runtimes with the -t flag, omit anything that has a zero milli-second runtime.
* Output the runtimes when performing a CVC regression test.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@624 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Tue, 2 Mar 2010 12:40:46 +0000 (12:40 +0000)]

* Merged in all the changes made to the bitblaster while I was working on it.
* Removed the BOOLVEC object type.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@623 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Mon, 1 Mar 2010 15:03:22 +0000 (15:03 +0000)]

First step of integrating Bitblasting to AIGs.
* The Bitblaster now produces BBNodes, not ASTNodes. Currently BBNodes are typedefed to ASTNodes.
* Improvements were made to the trunk's Bitblaster while I was working on this. I'll merge them in next.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@622 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Sun, 28 Feb 2010 11:39:33 +0000 (11:39 +0000)]

Adding nodefactory classes to libstp so that libast doesn't need to be explicitly included when using the c-interface.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@621 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

trevor_hansen [Sun, 28 Feb 2010 11:31:31 +0000 (11:31 +0000)]

Adding in test 21 to all.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@620 e59a4935-1847-0410-ae03-e826735625c1

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

commit | commitdiff | tree

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

STP Constraint Solver.