trevor_hansen [Sat, 12 Jun 2010 14:55:37 +0000 (14:55 +0000)]
Free up more memory before SAT solving. In particular this deletes the Tseitin variables before calling the SAT solver. This makes good sense for problems that aren't solved by abstraction / refinement. However, I'm not sure how it impacts difficult array problems.
trevor_hansen [Fri, 11 Jun 2010 02:04:18 +0000 (02:04 +0000)]
This makes SimplifyTerm idempotent. My hope is that this will reduce the number of times that the toplevel function needs to be called. If a term at the bottom of the graph doesn't map to itself when SimplifyTerm is run, then all the nodes above it will need to be re-created next time SimplifyTerm is called on the graph.
This patch adds an assertion function that isn't enabled.
trevor_hansen [Tue, 8 Jun 2010 12:52:46 +0000 (12:52 +0000)]
Bugfix. The bvsolver would replace a variable with an equation that contained that same variable. It did so because there was a special case that let it. I removed the special case.
I don't understand why the special case was there, so aren't sure if this will slow down some other instances?
trevor_hansen [Tue, 8 Jun 2010 11:28:27 +0000 (11:28 +0000)]
Copy the cleaner new SplitEven_into_Oddnum_PowerOf2 function from bvsolverExp. I'm comparing the values from the old and new version of the function still.
trevor_hansen [Sat, 29 May 2010 13:38:59 +0000 (13:38 +0000)]
Add my experimental BVSolver. It's much slower than the current bvsolver, but is more reliable. I'll gradually move its innovations into the main bvsolver.
trevor_hansen [Sat, 29 May 2010 05:52:37 +0000 (05:52 +0000)]
* Make the constant evaluator a non member function. This allows the simplifying node factory to use it without holding a reference to a Simplifier object.
* Change the simplifier to use the simplifying node factory by default.
trevor_hansen [Sat, 29 May 2010 04:22:11 +0000 (04:22 +0000)]
* Add a disabled-by-default option to simplify the arguments of a function first.
* Check explicitly the kind returned from some functions that create nodes to ensure the returned type is what we expect. With the simplifying node factory enabled, the type can sometimes change.
trevor_hansen [Fri, 28 May 2010 01:07:03 +0000 (01:07 +0000)]
Bugfix. If given bad input, the SMTLIB2 parser would match as much as it could then stop, without warning. It now checks that an end of file has been reached.
trevor_hansen [Fri, 21 May 2010 15:55:33 +0000 (15:55 +0000)]
An initial version of an smtlib2 format parser. It has these problems:
* Leaks memory
* Doesn't allow for annotations on terms.
* Ignores the commands sent to it. It just solves the problem specified.
Other changes:
* Long options are no longer case senstive.
* If the input file ends with .smt2 or .smt the appropriate parser is selected.
* The simplifying node factory is disabled during parsing when printing back is enabled. This allows STP to be used as a better, but still low-fidelity translator between formats.
trevor_hansen [Thu, 13 May 2010 05:40:09 +0000 (05:40 +0000)]
Remove the code for the "ReferenceCount". This was my first attempt to make the simplifications DAG-aware (sometimes called sharing-aware). The approach I chose was fundamentally broken (oops). I'm working on a new approach.
trevor_hansen [Thu, 13 May 2010 05:34:34 +0000 (05:34 +0000)]
* Use the simplifying node factory and the type checking node factory when parsing the CVC format via the main method. I haven't changed the c-interface to simplify as it build.
* Remove some explicit type checks in the CVC parser. Since the type checking node factory type checks each node it creates, there's no reason to have so many explicit type checks. So I've removed some of them.
trevor_hansen [Wed, 12 May 2010 14:29:38 +0000 (14:29 +0000)]
Add an encoding of multiplication that explicitly uses addition networks. This is copied from r482. I've not yet experimented with which bbmult() function is the best.
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
projects / francis / stp.git / log