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

msoos [Thu, 15 Apr 2010 12:52:17 +0000 (12:52 +0000)]

Merge branch 'newcrypto'

updated CMS2 so that segfault will no longer happen when UNSAT is found
in the middle of a varreplacement. The clause database was left in an
undefined state, which caused ~Solver to double-free some clauses

no longer be create

Conflicts:
src/sat/cryptominisat2/PartHandler.cpp
src/sat/cryptominisat2/Solver.cpp
src/sat/cryptominisat2/Solver.h
src/sat/cryptominisat2/Subsumer.cpp
src/sat/cryptominisat2/VERSION
src/sat/cryptominisat2/VarReplacer.cpp
src/sat/cryptominisat2/mtl/Vec.h

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

commit | commitdiff | tree

msoos [Wed, 14 Apr 2010 18:18:39 +0000 (18:18 +0000)]

Importing the new cryptominisat

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Apr 2010 14:20:49 +0000 (14:20 +0000)]

bugfix. r671 re-enabled checking counter-examples. However it checks the "query" which is sometimes (always ?) left undefined by the smtlib parser.

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Apr 2010 14:02:52 +0000 (14:02 +0000)]

Bugfix to r667. I discarded a variable instead of adding it into the solver map. This fixes the alvin.cvc problems (r666).

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Apr 2010 05:32:17 +0000 (05:32 +0000)]

Change a reference to a regular variable. This fixes an intermittent valgrind warning about accessing uninitialised memory

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Apr 2010 04:53:36 +0000 (04:53 +0000)]

* Bugfix. Fix the printed counterexample sometimes missing assignments, sometimes printing duplicate assignments.
* Updated the BoolVecToBVConst function to be faster.

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

commit | commitdiff | tree

trevor_hansen [Wed, 14 Apr 2010 01:43:48 +0000 (01:43 +0000)]

Bugfix. r284 or earlier removed checking of counter-examples. i.e. -d did nothing.

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

commit | commitdiff | tree

trevor_hansen [Tue, 13 Apr 2010 15:23:19 +0000 (15:23 +0000)]

If STP is compiled with minisat-core, add a command line option to enable simplifying minisat. This removes the need to separately compile a "simplifying minisat" version.

We now have two versions of STP: one for cryptominisat1/2 another for minisat/simplifying minisat.

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

commit | commitdiff | tree

trevor_hansen [Tue, 13 Apr 2010 14:18:06 +0000 (14:18 +0000)]

Remove unsound-minisat as per Vijay's advice.

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

commit | commitdiff | tree

smccam [Mon, 12 Apr 2010 19:36:49 +0000 (19:36 +0000)]

Add configuration options for selecting SAT solver, plus some related
cleanups to how scripts and Makefiles include and invoke each other.
Patch from Peter Collingbourne.

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Apr 2010 13:38:25 +0000 (13:38 +0000)]

Fix for failure reported by Alvin Cheung (r666)

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Apr 2010 12:32:50 +0000 (12:32 +0000)]

Disable expensive "and"/"or" simplifications in the simplifying node factory.

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Apr 2010 12:22:14 +0000 (12:22 +0000)]

Enable the simplifying node factory when parsing smt-lib format file.

BVConstEvaluator now does the logical operations too. I moved them over from CounterExample. I realise they no longer short-cut nicely, but don't believe it matters.

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Apr 2010 12:00:26 +0000 (12:00 +0000)]

This fixes things I broke in r662:
* Add ParserInterface.h which I missed.
* Revert back Makefile.common, which I didn't mean to change.
* Rename let-funcs in Makefile.in

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

commit | commitdiff | tree

trevor_hansen [Mon, 5 Apr 2010 06:41:01 +0000 (06:41 +0000)]

* Rename let-funcs.cpp to LetMgr.cpp
* Move the letMgr into the ParserInterface class. This means it's not in scope until the program exits, instead just during parsing.
* The smt-lib parser makes all its calls into STP via the ParserInterface class.
* Updated the smt-lib parser to use the typing node factory. Explicit calls to BVTypeCheck() are not longer required so have been removed.
* Removed some redundant type checks from the smt-lib parser.
* Updated the cvc parser to use the letmgr in the ParserInterface object.

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

commit | commitdiff | tree

smccam [Thu, 1 Apr 2010 20:01:52 +0000 (20:01 +0000)]

Specify default arguments only when compiling C++.
Patch from Peter Collingbourne.

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

commit | commitdiff | tree

smccam [Tue, 30 Mar 2010 18:46:06 +0000 (18:46 +0000)]

Call "make clean" *after* configure in clean-install.sh, rather than
before, so it has more of a chance of working.
Patch from Peter Collingbourne.

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

commit | commitdiff | tree

smccam [Tue, 30 Mar 2010 18:35:09 +0000 (18:35 +0000)]

Remove trailing comma at the end of an enumerator list, for pedantic
C++ compliance. Patch from Peter Collingbourne.

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

commit | commitdiff | tree

trevor_hansen [Tue, 30 Mar 2010 11:49:53 +0000 (11:49 +0000)]

Fix the command line flag to output the bench format.

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

commit | commitdiff | tree

vijay_ganesh [Wed, 24 Mar 2010 19:04:24 +0000 (19:04 +0000)]

added a bunch of crypto examples to stp-tests/broken/tooSlow, and a bunch of bio examples to stp-tests/broken/tooMuchMemory. This system of tracking slow examples is great

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

commit | commitdiff | tree

vijay_ganesh [Wed, 24 Mar 2010 16:21:28 +0000 (16:21 +0000)]

added more crypto tests to stp/tests/crypto-tests

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

commit | commitdiff | tree

vijay_ganesh [Mon, 22 Mar 2010 22:30:28 +0000 (22:30 +0000)]

commented out the mtrand initial seeding with time() function in sat/cryptominisat2/Solver.cpp. We introduced this to strongly randomize the assignments generated by STP

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

commit | commitdiff | tree

vijay_ganesh [Mon, 22 Mar 2010 22:26:51 +0000 (22:26 +0000)]

added new crypto tests, and perl-based crypto test generator in stp/tests/crypto-tests

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

commit | commitdiff | tree

smccam [Fri, 19 Mar 2010 02:23:59 +0000 (02:23 +0000)]

Add more destructors to the C interface, to help clients avoid memory
leaks. And fix a type so that linking works correctly.

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

commit | commitdiff | tree

smccam [Fri, 19 Mar 2010 02:22:03 +0000 (02:22 +0000)]

Exclude main/main.o from libstp.a.

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

commit | commitdiff | tree

smccam [Thu, 18 Mar 2010 23:56:46 +0000 (23:56 +0000)]

Oops, different fix for the same problem as r646. Actually Makefile is
still auto-generated, it's just that the source file has moved. So
"svn rm" and re-ignore the generated copy, and add a clarifying note
to the original.

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

commit | commitdiff | tree

smccam [Thu, 18 Mar 2010 23:43:50 +0000 (23:43 +0000)]

Remove obsolete top-level svn:ignore entries: since r119, Makefile is
not auto-generted and config.info is in scripts/.

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

commit | commitdiff | tree

smccam [Thu, 18 Mar 2010 23:25:15 +0000 (23:25 +0000)]

Update svn:ignore properties with "depend" and more other
auto-generated files.

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

commit | commitdiff | tree

trevor_hansen [Thu, 18 Mar 2010 15:04:33 +0000 (15:04 +0000)]

Output flags for bench format, and a rough CNF.

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

commit | commitdiff | tree

trevor_hansen [Wed, 17 Mar 2010 03:55:25 +0000 (03:55 +0000)]

When outputting to SMTLIB format handle properly some cases when the number of arguments > 2.

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

commit | commitdiff | tree

trevor_hansen [Sun, 14 Mar 2010 03:04:56 +0000 (03:04 +0000)]

* When printing in CVC format, traverse the nodes looking for symbols rather than using just the symbols that were parsed in. This makes it easier when converting from one format to another.
* Fix the SMTLIB printer, convert NAND to NOT(AND(.., typo on extrapred, convert pluses with >2 arguments into nested 2 argument pluses.
* Bugfix. Call print-back with the correct input function.

Note. GDL print-back isn't printing out the entire input expression. I'm not sure why.

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

commit | commitdiff | tree

trevor_hansen [Sat, 13 Mar 2010 12:32:40 +0000 (12:32 +0000)]

* Mark some single argument functions as commutative.
* Prevent duplicate constant nodes being created by the GDL printer.

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

commit | commitdiff | tree

trevor_hansen [Sat, 13 Mar 2010 12:09:05 +0000 (12:09 +0000)]

Cleanup after better after the lexer.

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

commit | commitdiff | tree

trevor_hansen [Sat, 13 Mar 2010 12:01:26 +0000 (12:01 +0000)]

Add command line arguments to print back gdl,dot,cvc and smtlib format.

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

commit | commitdiff | tree

trevor_hansen [Sat, 13 Mar 2010 11:58:58 +0000 (11:58 +0000)]

Fix the DIMACS CNF header

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

commit | commitdiff | tree

trevor_hansen [Wed, 10 Mar 2010 05:09:20 +0000 (05:09 +0000)]

* Fix the SMT-LIB format printer so that it produces correct output. STP can now function as a CVC to SMT-LIB translator.
* Cleanup the CVC format printer.
* Bugfix in the CVC format printer. Add brackets to some unary operations to enforce the correct precedence.
* Remove a un-unsed parameter from the CVC print-back.

To isolate the bug in the CVC format printer I used Robert Brummayer's excellent delta-debugger.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Mar 2010 14:51:16 +0000 (14:51 +0000)]

Allow lefshift by zero.

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

commit | commitdiff | tree

trevor_hansen [Tue, 9 Mar 2010 13:39:26 +0000 (13:39 +0000)]

Bugfix. Rightshift in CVC was broken. Thanks to Elnatan Reisner for the patch.

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

commit | commitdiff | tree

trevor_hansen [Sun, 7 Mar 2010 15:44:00 +0000 (15:44 +0000)]

Deleting the contents of the clause list before SAT solving

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

commit | commitdiff | tree

trevor_hansen [Sun, 7 Mar 2010 14:46:14 +0000 (14:46 +0000)]

Clear the contents of the BBTermMemo and BBFormMemo before calling the SAT solver.

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

commit | commitdiff | tree

trevor_hansen [Sun, 7 Mar 2010 14:31:11 +0000 (14:31 +0000)]

Removing unused inputs to the ToSAT class.

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

commit | commitdiff | tree

trevor_hansen [Sun, 7 Mar 2010 14:18:48 +0000 (14:18 +0000)]

Cosmetic changes.
* Make some methods private.
* Move the contents of CallSat into ToSat
* ifdef out some declarations.

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

commit | commitdiff | tree

trevor_hansen [Sun, 7 Mar 2010 14:07:42 +0000 (14:07 +0000)]

Fixing build. My last checkin forgot to add building "abc" to make all.

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

commit | commitdiff | tree

trevor_hansen [Sat, 6 Mar 2010 13:48:41 +0000 (13:48 +0000)]

Add the parts of the ABC system for sequential synthesis and verification that handles AIG (and-inverter graphs). This is just code related to managing AIGS and outputting them to CNF. This is version 070930 with only a syntactic change to remove a Valgrind warning.

NB: This is just the library. I haven't checked in the changes to STP to use the library.

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

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

STP Constraint Solver.