| 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 |
| 2010-07-06 |
trevor_hansen | * Interface changes for constant bit propagation. Not... |
commit | commitdiff | tree | snapshot |
| 2010-07-06 |
trevor_hansen | Fix. stp.a didn't have necessary cbitp file included... |
commit | commitdiff | tree | snapshot |
| 2010-07-06 |
trevor_hansen | Fix. The unit tests expect the cnf's to be called outpu... |
commit | commitdiff | tree | snapshot |
| 2010-07-06 |
trevor_hansen | Revert. In r915 I removed the default -m32 flag by... |
commit | commitdiff | tree | snapshot |
| 2010-07-05 |
trevor_hansen | More getting ready for constant bit propagation. This... |
commit | commitdiff | tree | snapshot |
| 2010-07-05 |
msoos | CryptoMiniSat can now be built |
commit | commitdiff | tree | snapshot |
| 2010-07-05 |
msoos | For low-cutoff speed reasons, it's best not to subsume... |
commit | commitdiff | tree | snapshot |
| 2010-07-05 |
trevor_hansen | Add the interface code for constant bit propagation... |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
msoos | Cleaning up some bugs in CryptoMS |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
trevor_hansen | Free the memory allocatated to the AIGs before SAT... |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
trevor_hansen | Tiny speedup. Generate the encoding of multiplication... |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
trevor_hansen | I didn't enable capturing of quick statistics (the... |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
trevor_hansen | Bugfix. The SMTLIB2 defines the outer bars (if present... |
commit | commitdiff | tree | snapshot |
| 2010-07-04 |
trevor_hansen | Get cryptominisat2 compiling: |
commit | commitdiff | tree | snapshot |
| 2010-07-03 |
trevor_hansen | Bitblast formula that don't contain arrays into and... |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Correcting small bug in CMS2 |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Updating CMS2 to get rid of a small bug |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Removing trailing code related to pools' #ifdefs in... |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Further updating of CryptoMiniSat2 |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Updating CryptoMiniSat2 to fix some minor bugs |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
msoos | Updating CryptoMiniSat2 |
commit | commitdiff | tree | snapshot |
| 2010-07-02 |
trevor_hansen | Rename the bitblaster class fron BitBlasterNew to BitBl... |
commit | commitdiff | tree | snapshot |
| 2010-07-01 |
trevor_hansen | Refactor, getting ready for AIGs. This does add additio... |
commit | commitdiff | tree | snapshot |
| 2010-06-29 |
trevor_hansen | Speedup. Generate nicer circuits for unsigned division. |
commit | commitdiff | tree | snapshot |
| 2010-06-28 |
trevor_hansen | Change how the counter example is built. Previously... |
commit | commitdiff | tree | snapshot |
| 2010-06-28 |
trevor_hansen | Speedup. Add solving for xors to the bitvector solver. |
commit | commitdiff | tree | snapshot |
| 2010-06-28 |
trevor_hansen | Speedup. if (xor a b) is found, replaced a with (not... |
commit | commitdiff | tree | snapshot |
| 2010-06-27 |
trevor_hansen | Speedup. Sort EQ nodes. This prevents duplicate nodes... |
commit | commitdiff | tree | snapshot |
| 2010-06-27 |
trevor_hansen | Speedup. Don't push extracts through ites. Sometimes... |
commit | commitdiff | tree | snapshot |
| 2010-06-27 |
trevor_hansen | Default to bash shell rather than sh for some calls... |
commit | commitdiff | tree | snapshot |
| 2010-06-27 |
trevor_hansen | Speedup. Revert back to minisat's default parameters. |
commit | commitdiff | tree | snapshot |
| 2010-06-27 |
trevor_hansen | Speedup. Flatten ands at the start of the bvsolver. |
commit | commitdiff | tree | snapshot |
| 2010-06-26 |
trevor_hansen | clean up two regression log names |
commit | commitdiff | tree | snapshot |
| next |