trevor_hansen [Wed, 12 May 2010 14:07:36 +0000 (14:07 +0000)]
First attempt at tracking time spent building the counter example. Doesn't properly include abstraction refinement checking time (I think). This introduces changes from r316
trevor_hansen [Fri, 7 May 2010 05:05:12 +0000 (05:05 +0000)]
Simplify the division operation. An unnecessary comparison has been removed from the division. This division as measured on the factoring12bitx12.cvc benchmark is about 20% faster.
vijay_ganesh [Thu, 6 May 2010 17:06:42 +0000 (17:06 +0000)]
fixed the problem with Alvin Cheung's testcase. The problem was that ITE-array expressions were not being handled correctly in SimplifyWrite_InPlace(). Fixed that
vijay_ganesh [Wed, 5 May 2010 16:33:47 +0000 (16:33 +0000)]
Perennial problem with svn. Does not give me the list of all modified files before check-in, and hence I end up checking-in experimental code. Fixed minor mod in STP.cpp
trevor_hansen [Wed, 5 May 2010 13:12:13 +0000 (13:12 +0000)]
Small changes to the array transformer:
* Use the node factory directly where possible.
* Use the general read(ite(...)..) case rather than handling specially read(write(ite...)..)..)
* Unless NDEBUG is defined check that no operations that should have been removed remain in the formula.
Hyper-binary resolution added binary clauses that lead to wrong UNSAT
answers, when the solution was in fact possible to find. I disabled it.
Also, other, minor problems have been fixed.
* Send the -t flag to STP when running regressstp. This outputs statistics that are useful to sum up.
* Delete my old eclipse formatting configuration. I don't use this anymore. Suspect no one else does either.
Simplification is carried if the problem seems difficult. It is carried
out in steps, so the complete algorithm's time demands do not have to
absorbed the first time it is run. Subpart-solving regularly checks for
parts of the problem that are disconnected, solves them, and returns to
the original problem instance -- essentially executing a
divide-and-conquer algorithm
Refactoring. This creates a separate ClauseList class that holds the pointers to the CNF's clauses. I've just moved stuff around, so nothing should break/ work better.
* Delete a test script that's no longer used
* regressstp now copies all the test cases to /dev/null to prime the disk cachde (like the other regression tests do).
* 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.
projects / francis / stp.git / log