]>
git.unchartedbackwaters.co.uk Git - francis/stp.git/log
trevor_hansen [Sat, 24 Apr 2010 12:06:16 +0000 (12:06 +0000)]
Fix leaks in the CVC parser
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@702
e59a4935 -1847-0410-ae03-
e826735625c1
trevor_hansen [Sat, 24 Apr 2010 09:54:10 +0000 (09:54 +0000)]
Fix memory leaks in the SMT-LIB parser.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@701
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 22 Apr 2010 11:34:23 +0000 (11:34 +0000)]
Updating CMS2 to fix some bugs
* Conglomerate was freeing the same clause. Fixed.
* Gaussian elimination is now disabled (was broken)
* Some code cleanup
* After solution extension, propagate was not called when decisionLevel
was 0. This lead to assertion failure when adding clause during
library usage
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@699
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Wed, 21 Apr 2010 10:44:06 +0000 (10:44 +0000)]
Updating CMS2 to correct destructor segfault
XorFinder left the state in an unstable manner when UNSAT was found this
later lead to a segfault when trying to destruct the solver. Fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@696
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 19 Apr 2010 10:12:30 +0000 (10:12 +0000)]
Fixing CMS2's library debug routine
It didn't work correctly when re-adding removed clauses: variable
elimination, conglomeration, and part-handling all dumped data, but they
shouldn't have been
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@693
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 19 Apr 2010 09:38:32 +0000 (09:38 +0000)]
Updating CMS2 to fix bug in Conglomerate.cpp
The Conglomeration aborted early when re-adding clauses, leading to a
bug that occured when UNSAT was found out while re-adding clauses. The
state of Conglomerate was left in a half-freed position, which lead to
Segfault when calling ~Conglomerate
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@692
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Mon, 19 Apr 2010 06:26:40 +0000 (06:26 +0000)]
CMS2 update missed out on the MTL library changes. Fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@691
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Sun, 18 Apr 2010 15:50:28 +0000 (15:50 +0000)]
CMS2 now has two types of learnt clause evaluation
CryptoMiniSat2 now has two types of learnt clause activity measures.
This means that different type of problems can be effectively solved
with the same solver that uses radically different measures of learnt
clause effectiveness. There are some rough edges for the moment: it's
really difficult which type of instance we are dealing with. So, the
'heuristic' that decides is really dumb. You can find it in
RestarTypeChooser.cpp. If you have a more refined heuristic in mind,
please share it with me!
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@688
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 16 Apr 2010 15:54:30 +0000 (15:54 +0000)]
Importing new version of CMS2
* bug with Conglomerate fixed. Conglomerate will in the future be
callable in the middle of solving
* variable activity is now uint32_t. No more floating point code.
This change also means a more conservative variable activity
heuristic. Should help on most problems (but not crypto, I
believe)
* Removed useless code around logging
* No more warnings on (deprecated) const char* to string conversion
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@687
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 16 Apr 2010 15:36:20 +0000 (15:36 +0000)]
Don't clean non-existing CryptoMiniSat1 dir
Cleaning script doesn't need to clean the 'cryptominisat' directory
since that doesn't exist any more. The clean script failed because of
this, fixed.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@686
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 16 Apr 2010 15:25:10 +0000 (15:25 +0000)]
Removing CryptoMiniSat ver. 1
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@685
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 16 Apr 2010 14:51:57 +0000 (14:51 +0000)]
Merge branch 'cryptominisat1_removed_and_rest_cleaned'
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@684
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Fri, 16 Apr 2010 12:59:14 +0000 (12:59 +0000)]
Updating CMS2 to fix two bugs
One was a bug relating to binarary xor-finding while doing failed
var searching: the xor-clauses were not cleaned beforehand.
The second bug was an inverted shrinking of memory contents in
operator= of Heap.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@683
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 15 Apr 2010 15:53:38 +0000 (15:53 +0000)]
CMS2 update: Extending the conglomerated clauses was done too early. Also, some non-decision variables were set for no reason in the model
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@680
e59a4935 -1847-0410-ae03-
e826735625c1
msoos [Thu, 15 Apr 2010 13:05:48 +0000 (13:05 +0000)]
Last commit contained some strange merging information that made a mess. Sorry, reverting.
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@679
e59a4935 -1847-0410-ae03-
e826735625c1
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
projects / francis / stp.git / log