| 2011-01-02 |
trevor_hansen | Cleanup / Speedup. Unnecessary work was done when build... |
commit | commitdiff | tree | snapshot |
| 2011-01-02 |
trevor_hansen | Bugfix. I didn't realise that the Flatten function... |
commit | commitdiff | tree | snapshot |
| 2011-01-02 |
trevor_hansen | Refactor. This shouldn't change anything |
commit | commitdiff | tree | snapshot |
| 2011-01-01 |
trevor_hansen | Speedup. The old Flatten was too slow. On an instance... |
commit | commitdiff | tree | snapshot |
| 2010-12-31 |
trevor_hansen | Extra assertion. Assert that internally created variabl... |
commit | commitdiff | tree | snapshot |
| 2010-12-31 |
trevor_hansen | Small leak fix. Didn't delete the variable introduced... |
commit | commitdiff | tree | snapshot |
| 2010-12-31 |
trevor_hansen | Fix the build. The speedup in the prior checkin needs... |
commit | commitdiff | tree | snapshot |
| 2010-12-31 |
trevor_hansen | Speedup. This makes it much faster to create some bvconsts. |
commit | commitdiff | tree | snapshot |
| 2010-12-31 |
trevor_hansen | Disable simplifications when printing back. I disabled... |
commit | commitdiff | tree | snapshot |
| 2010-12-21 |
trevor_hansen | Work around occasional hang with -g (when timing out). |
commit | commitdiff | tree | snapshot |
| 2010-12-18 |
smccam | Silence some legitimate warnings about int to pointer... |
commit | commitdiff | tree | snapshot |
| 2010-12-18 |
smccam | Makefile changes to improve the build of libstp.a.... |
commit | commitdiff | tree | snapshot |
| 2010-12-15 |
trevor_hansen | Adds a command line configuration option that is saved... |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Enable constant bit Propagation with CNF generation. |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Reduce the cutover for the advance CNF generator to... |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Enable constant bit propagation by default. |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Fix build. |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Maximally precise transfer functions for constant bit... |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | No longer default to -m32, causes too many problems |
commit | commitdiff | tree | snapshot |
| 2010-11-28 |
trevor_hansen | Patch from Markus Groß. Thanks. Here is the description... |
commit | commitdiff | tree | snapshot |
| 2010-11-06 |
trevor_hansen | Bugfix. simplifying-minisat failed when abstraction... |
commit | commitdiff | tree | snapshot |
| 2010-10-03 |
trevor_hansen | Fix. An optimisation added in r1020 was disabled. This... |
commit | commitdiff | tree | snapshot |
| 2010-10-01 |
trevor_hansen | Bugfix. Unsigned modulus of zero returned 1, it should... |
commit | commitdiff | tree | snapshot |
| 2010-09-24 |
trevor_hansen | Experimental. Push bvand and bvor through concats. |
commit | commitdiff | tree | snapshot |
| 2010-09-12 |
trevor_hansen | Bugfix. r1018 caused wrong answers. It left out a case... |
commit | commitdiff | tree | snapshot |
| 2010-09-12 |
trevor_hansen | Speedup. Add bvconcat normalisation. Break bvconcat... |
commit | commitdiff | tree | snapshot |
| 2010-09-12 |
trevor_hansen | Bugfix. The prior checkin cleaned up too much. Sometime... |
commit | commitdiff | tree | snapshot |
| 2010-09-12 |
trevor_hansen | Cleanup. Removes some clauses that must be "false". |
commit | commitdiff | tree | snapshot |
| 2010-09-12 |
trevor_hansen | Fix. Output the statistics for simplifying minisat. |
commit | commitdiff | tree | snapshot |
| 2010-09-10 |
trevor_hansen | When encoding to CNF via ABC, use the simple mapping... |
commit | commitdiff | tree | snapshot |
| 2010-09-08 |
trevor_hansen | Adds a Userflag to control whether the xor solver is... |
commit | commitdiff | tree | snapshot |
| 2010-09-07 |
trevor_hansen | Bugfix to the prior revision. Solving for 2 operand... |
commit | commitdiff | tree | snapshot |
| 2010-09-07 |
trevor_hansen | Experimental. Convert IFF to XOR during simplification... |
commit | commitdiff | tree | snapshot |
| 2010-09-03 |
vijay_ganesh | aligned the STP help printout (-h option). It is easier... |
commit | commitdiff | tree | snapshot |
| 2010-09-03 |
vijay_ganesh | aligned the STP help printout (-h option). It is easier... |
commit | commitdiff | tree | snapshot |
| 2010-08-31 |
trevor_hansen | Fresh variables created for internal uses, for instance... |
commit | commitdiff | tree | snapshot |
| 2010-08-31 |
trevor_hansen | Update the comments to match the last commit |
commit | commitdiff | tree | snapshot |
| 2010-08-31 |
trevor_hansen | Fix to the bvsolver. Some cases were missing when ident... |
commit | commitdiff | tree | snapshot |
| 2010-08-29 |
trevor_hansen | Bugfix in cbitp. Currently not enabled. |
commit | commitdiff | tree | snapshot |
| 2010-08-28 |
trevor_hansen | Fix error in experimental constant bit propagation... |
commit | commitdiff | tree | snapshot |
| 2010-08-28 |
trevor_hansen | Bugfix. Memory was sometimes read after it had been... |
commit | commitdiff | tree | snapshot |
| 2010-08-28 |
trevor_hansen | Fix. I thought the code I checked-in just now wasn... |
commit | commitdiff | tree | snapshot |
| 2010-08-28 |
trevor_hansen | Changes to inactive by default code. |
commit | commitdiff | tree | snapshot |
| 2010-08-22 |
trevor_hansen | Remove some assertion checks from code that's not enabl... |
commit | commitdiff | tree | snapshot |
| 2010-08-22 |
trevor_hansen | Bugfix. STP returned the wrong answer when something... |
commit | commitdiff | tree | snapshot |
| 2010-08-21 |
vijay_ganesh | minor changes to INSTALL instructions |
commit | commitdiff | tree | snapshot |
| 2010-08-20 |
trevor_hansen | Fix the build script |
commit | commitdiff | tree | snapshot |
| 2010-08-20 |
trevor_hansen | Remove variables from the configure script which contro... |
commit | commitdiff | tree | snapshot |
| 2010-08-20 |
trevor_hansen | Remove binaries I checked in by mistake |
commit | commitdiff | tree | snapshot |
| 2010-08-20 |
trevor_hansen | Fix build. Forgot to checkin these |
commit | commitdiff | tree | snapshot |
| 2010-08-20 |
trevor_hansen | * Replace minisat 2 with minisat 2.2. |
commit | commitdiff | tree | snapshot |
| 2010-08-18 |
trevor_hansen | Add regresssmtcomp2007 which runs the bitvector benchma... |
commit | commitdiff | tree | snapshot |
| 2010-08-18 |
trevor_hansen | Changes to inactive code. Use simple AIG simplification... |
commit | commitdiff | tree | snapshot |
| 2010-08-16 |
trevor_hansen | Update to currently inactive code. |
commit | commitdiff | tree | snapshot |
| 2010-08-16 |
trevor_hansen | Code for AIG rewriting with ABC. This code is not curre... |
commit | commitdiff | tree | snapshot |
| 2010-08-15 |
trevor_hansen | Extra tests for inactive by-default code |
commit | commitdiff | tree | snapshot |
| 2010-08-15 |
trevor_hansen | Refactor. Remove unncessary code. |
commit | commitdiff | tree | snapshot |
| 2010-08-15 |
trevor_hansen | Change non-enabled code. |
commit | commitdiff | tree | snapshot |
| 2010-08-14 |
trevor_hansen | Improvement? FlattenKind now recursively flattens it... |
commit | commitdiff | tree | snapshot |
| 2010-08-14 |
trevor_hansen | Should cause not runtime effects. |
commit | commitdiff | tree | snapshot |
| 2010-08-13 |
trevor_hansen | Speedup. Reduce the number of times that SortByArith... |
commit | commitdiff | tree | snapshot |
| 2010-08-11 |
trevor_hansen | Print out a not yet supported error. |
commit | commitdiff | tree | snapshot |
| 2010-08-11 |
trevor_hansen | Add a sorting network implementation. This code is... |
commit | commitdiff | tree | snapshot |
| 2010-08-10 |
trevor_hansen | Cleanup. Remove experimental (not active) code. |
commit | commitdiff | tree | snapshot |
| 2010-08-10 |
trevor_hansen | Improve the encoding of the full adder used by the... |
commit | commitdiff | tree | snapshot |
| 2010-08-10 |
trevor_hansen | Correct a comment |
commit | commitdiff | tree | snapshot |
| 2010-08-07 |
trevor_hansen | Bugfix. --output-CNF was broken when outputting with... |
commit | commitdiff | tree | snapshot |
| 2010-08-06 |
trevor_hansen | Fix slowdown. |
commit | commitdiff | tree | snapshot |
| 2010-08-05 |
trevor_hansen | Speedup the bvsolver. Use the applySubstitutionMap... |
commit | commitdiff | tree | snapshot |
| 2010-08-05 |
trevor_hansen | Bugfix. The prior revision sometimes returned the wrong... |
commit | commitdiff | tree | snapshot |
| 2010-08-01 |
trevor_hansen | Bugfix. Infinite loop. My fourth attempt to fix the... |
commit | commitdiff | tree | snapshot |
| 2010-07-31 |
trevor_hansen | Bugfix. Oops. When using the quick statistics (the... |
commit | commitdiff | tree | snapshot |
| 2010-07-28 |
trevor_hansen | Speedup. I've measured the performance of bit blasted... |
commit | commitdiff | tree | snapshot |
| 2010-07-28 |
trevor_hansen | Bugfix. Infinite loop. A third fix for r947. |
commit | commitdiff | tree | snapshot |
| 2010-07-28 |
trevor_hansen | Bugfix. STP may produce the wrong answer. Introduced... |
commit | commitdiff | tree | snapshot |
| 2010-07-28 |
trevor_hansen | Speed up of the unsigned division encoding. Update... |
commit | commitdiff | tree | snapshot |
| 2010-07-28 |
trevor_hansen | Refactoring. |
commit | commitdiff | tree | snapshot |
| 2010-07-26 |
trevor_hansen | Bugfix. Stop a null pointer error. |
commit | commitdiff | tree | snapshot |
| 2010-07-26 |
msoos | Further fixing of spurious printing in CryptoMiniSat |
commit | commitdiff | tree | snapshot |
| 2010-07-26 |
msoos | Fixing verbosity-related problems in CryptoMiniSat2 |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | A QF_ABV division has been added to the smt-lib. Update... |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Bugfix. Properly print out the counter example of booleans. |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Fix the build + extra options for constant bit propagat... |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Speedup. Flatten multiplications, sort, then re-assable... |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Extra code (not enabled), for constant bit propagation. |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Extra code (that's not currently enabled), so reduce... |
commit | commitdiff | tree | snapshot |
| 2010-07-10 |
trevor_hansen | Output quick statistics if enabled, and exiting after... |
commit | commitdiff | tree | snapshot |
| 2010-07-09 |
trevor_hansen | Decision. This optimisation helps our cvc regressions... |
commit | commitdiff | tree | snapshot |
| 2010-07-09 |
trevor_hansen | Add the option to exit after generating the CNF. Curren... |
commit | commitdiff | tree | snapshot |
| 2010-07-09 |
trevor_hansen | Bugfix. If a new-line occured in a string literal,... |
commit | commitdiff | tree | snapshot |
| 2010-07-08 |
petercol | Introduce vc_setInterfaceFlags function |
commit | commitdiff | tree | snapshot |
| 2010-07-08 |
trevor_hansen | Fix some small leaks when performing division by zero... |
commit | commitdiff | tree | snapshot |
| 2010-07-08 |
trevor_hansen | Only run the bvsolver if optimisations have been enable... |
commit | commitdiff | tree | snapshot |
| 2010-07-08 |
trevor_hansen | Fix the unit test script: |
commit | commitdiff | tree | snapshot |
| 2010-07-07 |
trevor_hansen | Bugfix. Remove a null pointer reference. |
commit | commitdiff | tree | snapshot |
| 2010-07-07 |
trevor_hansen | Simplify (bvdiv x x ) to one. Likewise for the other... |
commit | commitdiff | tree | snapshot |
| 2010-07-07 |
trevor_hansen | Fix the building of the stp library. |
commit | commitdiff | tree | snapshot |
| 2010-07-07 |
trevor_hansen | Fix the build. |
commit | commitdiff | tree | snapshot |
| 2010-07-07 |
trevor_hansen | Neaten up the code for constant bit propagation. Note... |
commit | commitdiff | tree | snapshot |
| 2010-07-06 |
trevor_hansen | Bugfix. Fix a check to ensure that the type of nodes... |
commit | commitdiff | tree | snapshot |
| next |