| 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 |
| 2011-03-26 |
trevor_hansen | Improvement. The simplifying node factory no longer... |
commit | commitdiff | tree | snapshot |
| 2011-03-25 |
trevor_hansen | Improvement. Convert left/right (NOT aritmetic), shifts... |
commit | commitdiff | tree | snapshot |
| 2011-03-25 |
trevor_hansen | Improvement. Better unsigned interval propagation of... |
commit | commitdiff | tree | snapshot |
| 2011-03-25 |
trevor_hansen | Fix remove an extra pair of brackets from LETs. Thanks... |
commit | commitdiff | tree | snapshot |
| 2011-03-24 |
trevor_hansen | Slight speedup to the hashing node factory. |
commit | commitdiff | tree | snapshot |
| 2011-03-24 |
trevor_hansen | Improvement. Create fewer objects. |
commit | commitdiff | tree | snapshot |
| 2011-03-24 |
trevor_hansen | Improvement. No longer have vectors in the ASTSymbol... |
commit | commitdiff | tree | snapshot |
| 2011-03-23 |
trevor_hansen | Speedup. Short cut before some copies were created. |
commit | commitdiff | tree | snapshot |
| 2011-03-23 |
trevor_hansen | Move CVC parser to using strings for LET names. Removes... |
commit | commitdiff | tree | snapshot |
| 2011-03-23 |
trevor_hansen | Improvement. SMTLIB2 lets now use strings for names... |
commit | commitdiff | tree | snapshot |
| 2011-03-23 |
trevor_hansen | Fix the SMTLIB1 to not accept badly formed input. Previ... |
commit | commitdiff | tree | snapshot |
| next |