| 2011-06-26 |
trevor_hansen | Improvement. Additional simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-06-23 |
trevor_hansen | Fix. Look for fatal errors when running tests. |
commit | commitdiff | tree | snapshot |
| 2011-06-23 |
trevor_hansen | Improvement. Simplifying minisat now uses the advanced... |
commit | commitdiff | tree | snapshot |
| 2011-06-22 |
trevor_hansen | Improvement. Create fewer clauses when creating an... |
commit | commitdiff | tree | snapshot |
| 2011-06-21 |
trevor_hansen | Automatically format this code. No semantic change. |
commit | commitdiff | tree | snapshot |
| 2011-06-21 |
trevor_hansen | Check axioms for indexes in order of the number of... |
commit | commitdiff | tree | snapshot |
| 2011-06-20 |
trevor_hansen | Improvement. During abstraction refinement process... |
commit | commitdiff | tree | snapshot |
| 2011-06-20 |
trevor_hansen | Fix. I forgot to remove the descriptions of -e -f from... |
commit | commitdiff | tree | snapshot |
| 2011-06-20 |
trevor_hansen | Remove the code for the not-working FOR construct. |
commit | commitdiff | tree | snapshot |
| 2011-06-20 |
trevor_hansen | Vijay advised we aren't going to do fors. |
commit | commitdiff | tree | snapshot |
| 2011-06-19 |
trevor_hansen | Use the advanced CNF generator to encode array problems... |
commit | commitdiff | tree | snapshot |
| 2011-06-16 |
trevor_hansen | Add boost to the licence, fix bitvector description. |
commit | commitdiff | tree | snapshot |
| 2011-06-16 |
trevor_hansen | Bugfix. Fix the semantics of BVSMOD to always give... |
commit | commitdiff | tree | snapshot |
| 2011-06-16 |
trevor_hansen | Speedup for easy instances. Don't call the SAT solver... |
commit | commitdiff | tree | snapshot |
| 2011-06-14 |
trevor_hansen | Add cloud9 test cases. |
commit | commitdiff | tree | snapshot |
| 2011-06-09 |
trevor_hansen | A windows patch to r446 from Hume. |
commit | commitdiff | tree | snapshot |
| 2011-05-12 |
trevor_hansen | Improvement. Make error checking more normal. |
commit | commitdiff | tree | snapshot |
| 2011-05-12 |
trevor_hansen | Extra simplification rule. |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Extra test cases that simplify down to nothing. |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | ITE context is mostly bad. Now disabled by default. |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | No longer default to the simple CNF generator for big... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Improvement. Exit-after-cnf would exit after sending... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Fix. Creating the node (v + v), where v is greater... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Bugfix. Arithmetic shifts by constants that didn't... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Revert the change to run_tests, I didn't mean to submit... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Remove the comment that 32-bit is best for arrays.... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Improvement. Add array size statistics when printing... |
commit | commitdiff | tree | snapshot |
| 2011-05-11 |
trevor_hansen | Bugfix. Maybe. Disable a comparison so that CNF convers... |
commit | commitdiff | tree | snapshot |
| 2011-05-09 |
trevor_hansen | Adds two extra simplfication rules. |
commit | commitdiff | tree | snapshot |
| 2011-05-09 |
trevor_hansen | More simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-05-07 |
trevor_hansen | Extra simplification rules for the simplifying node... |
commit | commitdiff | tree | snapshot |
| 2011-05-07 |
trevor_hansen | Signed division now returns what is should. Signed... |
commit | commitdiff | tree | snapshot |
| 2011-05-07 |
trevor_hansen | Add a public function that calls sizeReducing until... |
commit | commitdiff | tree | snapshot |
| 2011-05-05 |
trevor_hansen | Adds an extra BVPLUS simplification rule. Cleans up... |
commit | commitdiff | tree | snapshot |
| 2011-05-05 |
trevor_hansen | Important bugfix. r1291 through to this revision, about... |
commit | commitdiff | tree | snapshot |
| 2011-05-05 |
trevor_hansen | Add an extra simplification rule. |
commit | commitdiff | tree | snapshot |
| 2011-05-04 |
trevor_hansen | Replace variables before calling the interval analysis. |
commit | commitdiff | tree | snapshot |
| 2011-05-04 |
trevor_hansen | Function to reset the stopwatch. |
commit | commitdiff | tree | snapshot |
| 2011-05-04 |
trevor_hansen | Another fix to the same |
commit | commitdiff | tree | snapshot |
| 2011-05-04 |
trevor_hansen | Correct the last patch. I don't think this code runs. |
commit | commitdiff | tree | snapshot |
| 2011-05-04 |
trevor_hansen | Apply simplifications through arrayterms too. |
commit | commitdiff | tree | snapshot |
| 2011-05-02 |
trevor_hansen | Bugfix. Rarely we get the wrong answer; I got two broke... |
commit | commitdiff | tree | snapshot |
| 2011-05-01 |
trevor_hansen | Compiling with -D_GLIBCXX_DEBUG reported warnings becau... |
commit | commitdiff | tree | snapshot |
| 2011-05-01 |
trevor_hansen | Code to apply the alwaysTrueSet. Not currently enabled. |
commit | commitdiff | tree | snapshot |
| 2011-05-01 |
trevor_hansen | Enable bitblast simplifications by default |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Turn off the ite-context simplification by default. |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Important Bugfix. The prior checkin sometimes, but... |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Bugfix. The last checkin caused an infinite loop (often). |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Extra simplification rules |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Extra simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-04-30 |
trevor_hansen | Convert subtraction to addition in the simplifying... |
commit | commitdiff | tree | snapshot |
| 2011-04-29 |
trevor_hansen | Bugfix. Reads might have been simplified down which... |
commit | commitdiff | tree | snapshot |
| 2011-04-27 |
trevor_hansen | Important Bugfix. The prior checkin causes the WRONG... |
commit | commitdiff | tree | snapshot |
| 2011-04-27 |
trevor_hansen | Extra simplification rules. In particular a simple... |
commit | commitdiff | tree | snapshot |
| 2011-04-27 |
trevor_hansen | Add extra simplifying rules. |
commit | commitdiff | tree | snapshot |
| 2011-04-27 |
trevor_hansen | Fix. I thought that extracts don't add any information... |
commit | commitdiff | tree | snapshot |
| 2011-04-27 |
trevor_hansen | Remove signed division, modulus and remainder when... |
commit | commitdiff | tree | snapshot |
| 2011-04-26 |
trevor_hansen | Two extra simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-04-21 |
trevor_hansen | Change the sorting network based adder (which isn't... |
commit | commitdiff | tree | snapshot |
| 2011-04-20 |
trevor_hansen | Refactor. Less verbose. |
commit | commitdiff | tree | snapshot |
| 2011-04-20 |
trevor_hansen | Improvement. Add a warning when parsing problems that... |
commit | commitdiff | tree | snapshot |
| 2011-04-16 |
trevor_hansen | Extra upfront simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-04-14 |
trevor_hansen | Add some missing simplification rules for AND/OR/ propo... |
commit | commitdiff | tree | snapshot |
| 2011-04-14 |
trevor_hansen | Shortcut in a rare circumstance. |
commit | commitdiff | tree | snapshot |
| 2011-04-14 |
trevor_hansen | Extra BVXOR simplification rules. |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Adds the reverse of rules to catch an obscure but impor... |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Improvement. Add a warning message when using --exit... |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Improvement. Fix the difficulty score for subtraction. |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Fix the build. Without -NDEBUG wouldn't compile. |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Improvement. Look for nodes that are true/false when... |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Remove some assertions that don't necessarily hold. |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Improvement. Replace the hashing node factory with... |
commit | commitdiff | tree | snapshot |
| 2011-04-13 |
trevor_hansen | Extra simplification rule. |
commit | commitdiff | tree | snapshot |
| 2011-04-11 |
trevor_hansen | oops. Meant to add this too. |
commit | commitdiff | tree | snapshot |
| 2011-04-11 |
trevor_hansen | Add an extra simplification rule to the simplifying... |
commit | commitdiff | tree | snapshot |
| 2011-04-11 |
trevor_hansen | Move some division be zero code into the bitblaster... |
commit | commitdiff | tree | snapshot |
| 2011-04-10 |
trevor_hansen | Adds code, that's not currently enabled, to read-out... |
commit | commitdiff | tree | snapshot |
| 2011-04-10 |
trevor_hansen | Improvement. Use the simplifying node factory in transf... |
commit | commitdiff | tree | snapshot |
| 2011-04-10 |
trevor_hansen | Revert the previous revision. It broke lots. |
commit | commitdiff | tree | snapshot |
| 2011-04-08 |
trevor_hansen | Improvement. Use the simplifying node factory in transf... |
commit | commitdiff | tree | snapshot |
| 2011-04-08 |
trevor_hansen | Improvement. Don't add NOT FALSE at the end of the... |
commit | commitdiff | tree | snapshot |
| 2011-04-07 |
trevor_hansen | Improvement. When a node is simplified set a value... |
commit | commitdiff | tree | snapshot |
| 2011-04-07 |
trevor_hansen | Improvement. Output the time spent in a stage with -s. |
commit | commitdiff | tree | snapshot |
| 2011-04-07 |
trevor_hansen | Hack. The ITE context simplification blows out ff.stp... |
commit | commitdiff | tree | snapshot |
| 2011-04-07 |
trevor_hansen | Revert. I didn't mean to checkin all those changes. |
commit | commitdiff | tree | snapshot |
| 2011-04-07 |
trevor_hansen | Hack. The ITE context simplification blows out ff.stp... |
commit | commitdiff | tree | snapshot |
| 2011-04-06 |
trevor_hansen | Remove junk. |
commit | commitdiff | tree | snapshot |
| 2011-04-06 |
trevor_hansen | Improve the bvsolver.If the substitution of a monomial... |
commit | commitdiff | tree | snapshot |
| 2011-04-06 |
trevor_hansen | Refactor. Remove junk. |
commit | commitdiff | tree | snapshot |
| 2011-04-03 |
trevor_hansen | Improvement. Some extra simplifications for the simplif... |
commit | commitdiff | tree | snapshot |
| 2011-04-03 |
trevor_hansen | Improvement. The simplifying node factory never creates... |
commit | commitdiff | tree | snapshot |
| 2011-03-31 |
trevor_hansen | Tiny improvement. Add the one-bit operations that evalu... |
commit | commitdiff | tree | snapshot |
| 2011-03-31 |
trevor_hansen | Small improvement. Discard the inner write if the two... |
commit | commitdiff | tree | snapshot |
| 2011-03-29 |
trevor_hansen | Work around rare problem caused by the simplifying... |
commit | commitdiff | tree | snapshot |
| 2011-03-28 |
trevor_hansen | Make applySubstitutionMap idempotent (I hope). |
commit | commitdiff | tree | snapshot |
| 2011-03-28 |
trevor_hansen | Improvement. The simplifying node factory now eliminate... |
commit | commitdiff | tree | snapshot |
| 2011-03-28 |
trevor_hansen | During the size reducing transformations, now set the... |
commit | commitdiff | tree | snapshot |
| 2011-03-28 |
trevor_hansen | Change the names for some statistics. |
commit | commitdiff | tree | snapshot |
| 2011-03-28 |
trevor_hansen | Extra simplification rule for BVXOR. |
commit | commitdiff | tree | snapshot |
| 2011-03-27 |
trevor_hansen | Add experimental code (not presently enabled), that... |
commit | commitdiff | tree | snapshot |
| next |