* Make regressall depend on "all". If any changes have occured to STP's source code before you test, there will be a rebuilt. This prevents the problem of testing an old version of STP.
* Fix the regressstp target. It wasn't outputting to the log file.
Reverting r465. Based on Stephen's example: stp-tests/crypto-tests/factoring-12bitsx12.stp this makes division about 50% faster.
Confirming what Stephen identified, varying just the bvdiv encoding:
crypto2: 42sec vs 32sec
simplifying minisat: 65s vs 37s
core minisat: 65s vs 43s
However, r600 solved this problem the fastest I've seen: 14 seconds. But that was cryptominisat. Cryptominisat2 is now in the trunk. So I suspect that this reverts a change that made division faster on cryptominisat, but slowed it down on the others (including cryptominisat2).
* 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
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
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
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!
* 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
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
* Bugfix. Fix the printed counterexample sometimes missing assignments, sometimes printing duplicate assignments.
* Updated the BoolVecToBVConst function to be faster.
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.
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.
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.
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
* 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.
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
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
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
projects / francis / stp.git / log